Update des oracles

Mise à jour des oracles de alluses après bugfix, ajout des oracles
pour le critère ASSERT (beta)

Makefile

@@ -27,8 +27,6 @@ PLUGIN_NAME      = LAnnotate
 PLUGIN_BFLAGS += -warn-error -a
 PLUGIN_OFLAGS += -warn-error -a
 
-PLUGIN_DEPENDENCIES += Stady
-
 PLUGIN_TESTS_DIRS:= options criteria
 
 PLUGIN_CMO = options utils ast_const bes simplify annotators wm \

README.markdown

@@ -58,7 +58,7 @@ Authors
 - Omar Chebaro
 - Mickaël Delahaye
 - Michaël Marcozzi
-
+- Thibault Martin
 Also many thanks to the rest of LTest's team:
 - Nikolai Kosmatov
 - Sébastien Bardin

register.ml

@@ -65,8 +65,8 @@ let annotate_on_project ann_names =
   Annotators.annotate (compute_outfile (Options.Output.get ()) (Kernel.Files.get ())) ann_names ~collect (Ast.get ());
 
 
-  let annotations = !annotations in
   if not !Annotators.assertDone then begin
+    let annotations = !annotations in
     (* output modified c file *)
     Options.feedback "write modified C file (to %s)" filename;
     let out = open_out filename in

tests/criteria/oracle/test_ASSERT.res.oracle

+[kernel] Parsing tests/criteria/test_ASSERT.c (with preprocessing)

tests/criteria/oracle/test_ASSERT_labels.c

+#include "/usr/local/share/frama-c/stady/externals.h"
+
+int main_precond(int a, int b) {
+  return 1;
+  
+}
+int main(int a, int b)
+{
+  int old_a;
+  int old_b;
+  old_a = a;
+  old_b = b;
+  {
+    int __retres;
+    if (a && b) {
+      {
+        {
+          mpz_t __sd_Z_to_Z_0;
+          mpz_t __sd_Z_cst_0;
+          int __sd_eq_0;
+          int __sd_or_0;
+          __gmpz_init_set_si(__sd_Z_to_Z_0,a);
+          __gmpz_init_set_str(__sd_Z_cst_0,"0",10);
+          __sd_eq_0 = __gmpz_cmp(__sd_Z_to_Z_0,__sd_Z_cst_0);
+          __sd_or_0 = __sd_eq_0 == 0;
+          if (! __sd_or_0) {
+            mpz_t __sd_Z_to_Z_1;
+            mpz_t __sd_Z_cst_1;
+            int __sd_eq_1;
+            __gmpz_init_set_si(__sd_Z_to_Z_1,b);
+            __gmpz_init_set_str(__sd_Z_cst_1,"0",10);
+            __sd_eq_1 = __gmpz_cmp(__sd_Z_to_Z_1,__sd_Z_cst_1);
+            __sd_or_0 = __sd_eq_1 == 0;
+            __gmpz_clear(__sd_Z_to_Z_1);
+            __gmpz_clear(__sd_Z_cst_1);
+          }
+          pc_label(! __sd_or_0,0,"ASSERT");
+          __gmpz_clear(__sd_Z_to_Z_0);
+          __gmpz_clear(__sd_Z_cst_0);
+          
+        }
+        ;
+        __retres = a + 1;
+        goto return_label;
+      }
+    }
+    else {
+      {
+        {
+          mpz_t __sd_Z_to_Z_2;
+          mpz_t __sd_Z_cst_2;
+          int __sd_eq_2;
+          int __sd_or_1;
+          __gmpz_init_set_si(__sd_Z_to_Z_2,a);
+          __gmpz_init_set_str(__sd_Z_cst_2,"0",10);
+          __sd_eq_2 = __gmpz_cmp(__sd_Z_to_Z_2,__sd_Z_cst_2);
+          __sd_or_1 = __sd_eq_2 == 0;
+          if (! __sd_or_1) {
+            mpz_t __sd_Z_to_Z_3;
+            mpz_t __sd_Z_cst_3;
+            int __sd_eq_3;
+            __gmpz_init_set_si(__sd_Z_to_Z_3,b);
+            __gmpz_init_set_str(__sd_Z_cst_3,"0",10);
+            __sd_eq_3 = __gmpz_cmp(__sd_Z_to_Z_3,__sd_Z_cst_3);
+            __sd_or_1 = __sd_eq_3 == 0;
+            __gmpz_clear(__sd_Z_to_Z_3);
+            __gmpz_clear(__sd_Z_cst_3);
+          }
+          pc_label(! __sd_or_1,1,"ASSERT");
+          __gmpz_clear(__sd_Z_to_Z_2);
+          __gmpz_clear(__sd_Z_cst_2);
+          
+        }
+        ;
+        __retres = b;
+        goto return_label;
+      }
+    }
+    
+    return_label: return __retres;
+  }
+}

tests/criteria/oracle/test_ASSERT_labels.labels

+# id, status, tag, origin_loc, current_loc, emitter, exec_time
+0,unknown,ASSERT,/home/tmartin/Documents/Labels/lannotate/tests/criteria/test_ASSERT.c:11,,lannot,0.
+1,unknown,ASSERT,/home/tmartin/Documents/Labels/lannotate/tests/criteria/test_ASSERT.c:15,,lannot,0.

tests/criteria/oracle/test_ASSERT_output.log

+[kernel] Parsing tests/criteria/test_ASSERT.c (with preprocessing)
+[lannot] start project default_labels
+[kernel] Parsing tests/criteria/test_ASSERT.c (with preprocessing)
+[lannot] apply annotations for ASSERT
+[stady] write label data (to tests/criteria/test_ASSERT_labels.labels)
+[stady] write modified C file (to tests/criteria/test_ASSERT_labels.c)
+[stady] finished

tests/criteria/oracle/test_alluses_labels.c

@@ -64,13 +64,11 @@ int maintest(int c)
       a = 3;
       pc_label_sequence(1,3434,1,2,"51",0);
       pc_label_sequence(1,2798,1,2,"51",0);
-      pc_label_sequence(1,3602,2,2,"52",0);
       pc_label_sequence(1,3028,2,2,"52",0);
       pc_label_sequence(1,2575,2,2,"52",0);
       pc_label_sequence_condition(0,"52");
       b = b;
       pc_label_sequence(1,4412,1,2,"52",0);
-      pc_label_sequence(1,3602,1,2,"52",0);
     }
     else {
       pc_label_sequence(1,2798,2,2,"51",0);

tests/criteria/oracle/test_alluses_labels.hyperlabels

 <s2434.s2029.s1719.s1489|; ;>,
 <s3107.s2575.s2158.s1838.s1600|; ;>,
 <s3688.s3028.s2503.s2092|; ;>,
-<s4412.s3602|; ;>,
+<s4412|; ;>,
 <s5303|; ;>,
 <s2093.s1778.s1544|; ;>,
 <s2433.s2028|; ;>,

tests/criteria/oracle/test_alluses_output.log

@@ -3,7 +3,7 @@
 [kernel] Parsing tests/criteria/test_alluses.c (with preprocessing)
 [lannot] apply annotations for alluses
 [lannot] write hyperlabel data (to tests/criteria/result/test_alluses_labels.hyperlabels)
-[lannot] Total number of labels = 50
+[lannot] Total number of labels = 48
 [lannot] finished
 [lannot] write modified C file (to tests/criteria/result/test_alluses_labels.c)
 [lannot] write label data (to tests/criteria/result/test_alluses_labels.labels)

tests/criteria/test_ASSERT.c

+/* run.config
+   EXECNOW: LOG @PTEST_NAME@_labels.c LOG @PTEST_NAME@_labels.labels LOG @PTEST_NAME@_output.log @frama-c@ -lannot=ASSERT -lannot-debug 1 @PTEST_DIR@/@PTEST_NAME@.c > @PTEST_DIR@/result/@PTEST_NAME@_output.log
+   EXECNOW: mv @PTEST_DIR@/@PTEST_NAME@_labels.c @PTEST_DIR@/result/@PTEST_NAME@_labels.c
+   EXECNOW: mv @PTEST_DIR@/@PTEST_NAME@_labels.labels @PTEST_DIR@/result/@PTEST_NAME@_labels.labels
+ */
+
+#include "limits.h"
+
+int main(int a, int b){
+	if(a && b){
+		//@ assert !a || !b;
+		return a+1;
+	 }
+	else
+		//@ assert !a || !b; 
+		return b;
+}