Frontend does not handle fscanf of stdin correctly
There seems to be a regression in our frontend, since fscanf(stdin,...) is no longer being handled correctly for ../../sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int64_t_fscanf_add_01_bad.i for predicate analysis for overflows.
For the same command-line I get differing results:
bin/cpachecker --svcomp25 --heap 10000M --benchmark --timelimit '900 s' --spec ../../sv-benchmarks/c/properties/no-overflow.prp --64 ../../sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int64_t_fscanf_add_01_bad.i
For version 4.0 of CPAchecker of CPAchecker, I get the following output:
Verification result: FALSE. Property violation (no-overflow: integer overflow in line 1555) found by chosen configuration.
while for version `` of CPAchecker I get:
Error: line 1553: Unrecognized C code (First parameter of fscanf() must be a FILE*): fscanf(stdin, "%ld", &data) (line was originally fscanf (stdin, "%" "l" "d", &data);) (ExpressionToFormulaVisitor.validateFscanfParameters, SEVERE)
Verification result: UNKNOWN, incomplete analysis.