From 1f8a287f21d5884e78edc81fe59bfa0714d7abe2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 23 Feb 2024 10:23:58 +0100
Subject: [PATCH] [ir2cabs] emulate and/or normalization done by FC's own ACSL
parser
See frama-c/frama-c#1364
---
convert_acsl.ml | 27 ++++++++++++++++++++----
tests/basic/oracle/cxx_c_link.res.oracle | 4 ----
tests/specs/cxx_c_acsl.c | 13 ++++++++++++
tests/specs/cxx_c_acsl.cpp | 6 ++++++
tests/specs/oracle/cxx_c_acsl.res.oracle | 17 +++++++++++++++
5 files changed, 59 insertions(+), 8 deletions(-)
create mode 100644 tests/specs/cxx_c_acsl.c
create mode 100644 tests/specs/cxx_c_acsl.cpp
create mode 100644 tests/specs/oracle/cxx_c_acsl.res.oracle
diff --git a/convert_acsl.ml b/convert_acsl.ml
index 0e9ed0a6..c844ea36 100644
--- a/convert_acsl.ml
+++ b/convert_acsl.ml
@@ -232,6 +232,25 @@ let convert_logic_reference env typ e =
PLunop(Ustar, full_e)
| _ -> e
+(* ACSL parser normalizes conjunctions and disjunctions. We do the same here
+ in order to ensure syntactical equality of ACSL predicates
+ when parsed either directly or through framaCIRGen in an extern "C". *)
+let rec pland ce1 ce2 =
+ match ce2.lexpr_node with
+ | PLand(ce3,ce4) ->
+ let lexpr_loc = fst ce1.lexpr_loc, snd ce3.lexpr_loc in
+ let lexpr_node = pland ce1 ce3 in
+ PLand ({ lexpr_loc; lexpr_node}, ce4)
+ | _ -> PLand (ce1, ce2)
+
+let rec plor ce1 ce2 =
+ match ce2.lexpr_node with
+ | PLor(ce3, ce4) ->
+ let lexpr_loc = fst ce1.lexpr_loc, snd ce3.lexpr_loc in
+ let lexpr_node = plor ce1 ce3 in
+ PLor ({ lexpr_loc; lexpr_node }, ce4)
+ | _ -> PLor (ce1, ce2)
+
let rec convert_logic_expr env e =
let env = Convert_env.set_loc env e.loc in
let lexpr_loc = Convert_env.get_loc env in
@@ -283,11 +302,11 @@ and convert_logic_expr_node env = function
| TBinOp(BOLogicalAnd,e1,e2) ->
let env, ce1 = convert_logic_expr env e1 in
let env, ce2 = convert_logic_expr env e2 in
- env, PLand(ce1,ce2)
+ env, pland ce1 ce2
| TBinOp(BOLogicalOr,e1,e2) ->
let env, ce1 = convert_logic_expr env e1 in
let env, ce2 = convert_logic_expr env e2 in
- env, PLor(ce1,ce2)
+ env, plor ce1 ce2
| TBinOp _ -> Convert_env.fatal env "Unknown binary operator in logic"
| TCastE(typ,e) ->
let env, ctyp = convert_logic_type env typ in
@@ -487,11 +506,11 @@ and convert_pred env = function
| Pand(p1,p2) ->
let env, p1 = convert_pred_named env p1 in
let env, p2 = convert_pred_named env p2 in
- env, PLand(p1,p2)
+ env, pland p1 p2
| Por(p1,p2) ->
let env, p1 = convert_pred_named env p1 in
let env, p2 = convert_pred_named env p2 in
- env, PLor(p1,p2)
+ env, plor p1 p2
| Pxor(p1,p2) ->
let env, p1 = convert_pred_named env p1 in
let env, p2 = convert_pred_named env p2 in
diff --git a/tests/basic/oracle/cxx_c_link.res.oracle b/tests/basic/oracle/cxx_c_link.res.oracle
index 247cba88..82252579 100644
--- a/tests/basic/oracle/cxx_c_link.res.oracle
+++ b/tests/basic/oracle/cxx_c_link.res.oracle
@@ -1,10 +1,6 @@
[kernel] Parsing cxx_c_link.cpp (external front-end)
Now output intermediate result
[kernel] Parsing cxx_c_link.c (with preprocessing)
-[kernel] FRAMAC_SHARE/libc/stdlib.h:322: Warning:
- found two contracts. Merging them
-[kernel] FRAMAC_SHARE/libc/stdlib.h:330: Warning:
- found two contracts. Merging them
/* Generated by Frama-C */
#include "__fc_alloc_axiomatic.h"
#include "stdlib.h"
diff --git a/tests/specs/cxx_c_acsl.c b/tests/specs/cxx_c_acsl.c
new file mode 100644
index 00000000..30d915ed
--- /dev/null
+++ b/tests/specs/cxx_c_acsl.c
@@ -0,0 +1,13 @@
+/* run.config
+DONTRUN: main test is the .cpp file
+*/
+
+//@ predicate test1(double x) = \is_finite(x) && 0.0 < x && x < 2.0;
+
+//@ predicate test2(double x) = \is_finite(x) && 0.0 < x < 2.0;
+
+//@ predicate test3(double x) = (\is_finite(x) && 0.0 < x) && x < 2.0;
+
+//@ predicate test4(double x) = \is_finite(x) && (0.0 < x && x < 2.0);
+
+//@ predicate test5(double x) = (\is_finite(x) && 0.0 < x) && (x < 2.0 && \is_finite(x));
diff --git a/tests/specs/cxx_c_acsl.cpp b/tests/specs/cxx_c_acsl.cpp
new file mode 100644
index 00000000..c7cec0e2
--- /dev/null
+++ b/tests/specs/cxx_c_acsl.cpp
@@ -0,0 +1,6 @@
+/* run.config
+OPT: %{dep:@PTEST_DIR@/@PTEST_NAME@.c} -print
+*/
+extern "C" {
+#include "cxx_c_acsl.c"
+}
diff --git a/tests/specs/oracle/cxx_c_acsl.res.oracle b/tests/specs/oracle/cxx_c_acsl.res.oracle
new file mode 100644
index 00000000..135f9fd8
--- /dev/null
+++ b/tests/specs/oracle/cxx_c_acsl.res.oracle
@@ -0,0 +1,17 @@
+[kernel] Parsing cxx_c_acsl.cpp (external front-end)
+Now output intermediate result
+[kernel] Parsing cxx_c_acsl.c (with preprocessing)
+/* Generated by Frama-C */
+/*@ predicate test1(double x) = \is_finite(x) ∧ 0.0 < x < 2.0;
+ */
+/*@ predicate test2(double x) = \is_finite(x) ∧ 0.0 < x < 2.0;
+ */
+/*@ predicate test3(double x) = \is_finite(x) ∧ 0.0 < x < 2.0;
+ */
+/*@ predicate test4(double x) = \is_finite(x) ∧ 0.0 < x < 2.0;
+ */
+/*@
+predicate test5(double x) =
+ \is_finite(x) ∧ 0.0 < x < 2.0 ∧ \is_finite(x);
+ */
+
--
GitLab