[ir2cabs] emulate and/or normalization done by FC's own ACSL parser

See frama-c/frama-c#1364

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

tests/basic/oracle/cxx_c_link.res.oracle

 [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"

tests/specs/cxx_c_acsl.c

+/* 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));

tests/specs/cxx_c_acsl.cpp

+/* run.config
+OPT: %{dep:@PTEST_DIR@/@PTEST_NAME@.c} -print
+*/
+extern "C" {
+#include "cxx_c_acsl.c"
+}

tests/specs/oracle/cxx_c_acsl.res.oracle

+[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);
+ */
+