[e-acsl] fix untyped arguments due to exception
In an application, when during the typing of an earlier argument an exception is raised (e.g. due to an unsupported language construct) the remaining arguments are not typed. This can lead to exceptions in later stages (e.g. translation) with misleading/uninformative error messages like: [e-acsl] Failure: typing was not performed on construct n Therefore we now type all arguments even if the typing of an earlier argument fails. We re-raise the first encountered exception. Fixes #1388 An example that causes this behaviour: /* run.config COMMENT: see https://git.frama-c.com/frama-c/frama-c/-/issues/1388 COMMENT: The constant 1 remained untyped because the typing of strlen(s) COMMENT: raised an exception */ #include <string.h> /*@ logic ℤ fst(ℤ i, ℤ j) = i; logic ℤ f(char *s, ℤ n) = fst(strlen(s), 1); */ int main() { /*@ assert f("abc", 3) == 0; */ return 0; }
Loading
Please register or sign in to comment