From 76b085ea6a860656623859f3e879e0513fcd496d Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Wed, 10 Apr 2024 13:35:50 +0200
Subject: [PATCH] [e-acsl] fix untyped arguments due to exception
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
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;
}
---
src/plugins/e-acsl/src/analyses/typing.ml | 18 +++++++++++++++---
1 file changed, 15 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 8849626ac5b..794bc0e0452 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -530,6 +530,18 @@ let rec type_term
?ctx
~profile x)
in
+ let type_args type_arg =
+ (* type all arguments using typing function [type_arg] while
+ making sure that later arguments are typed even if an exception is
+ raised during the typing of an earlier argument. *)
+ let exn_o = ref None in
+ let type_arg arg =
+ try type_arg arg
+ with exn -> match !exn_o with None -> exn_o := Some exn | Some _ -> ()
+ in
+ List.iter (fun arg -> type_arg arg) args;
+ Option.iter raise !exn_o
+ in
if Builtins.mem li.l_var_info.lv_name then
let typ_arg lvi arg =
(* a built-in is a C function, so the context is necessarily a C
@@ -550,7 +562,7 @@ let rec type_term
| LBpred p ->
(* possible to have an [LBpred] here because we transformed
[Papp] into [Tapp] *)
- List.iter type_arg args;
+ type_args type_arg;
let new_profile =
Profile.make
li.l_profile
@@ -562,7 +574,7 @@ let rec type_term
pending_typing;
c_int
| LBterm t_body ->
- List.iter type_arg args;
+ type_args type_arg;
let new_profile =
Profile.make
li.l_profile
@@ -633,7 +645,7 @@ let rec type_term
let type_arg arg =
ignore @@ type_term ~use_gmp_opt:true ~arith_operand:false ~profile arg
in
- List.iter type_arg args;
+ type_args type_arg;
(* TODO : improve error message to distinguish error messages
corresponding to unsupported primitives and wrong application
of supported primitive
--
GitLab