Ported to TPM

advanced/assembly1.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile analyzer assembly1.c -gui
+// tis gui assembly1
 
 #include <stdio.h>
 

advanced/assembly2.c

@@ -1,5 +1,5 @@
 // make assembly2 && ./assembly2 && rm assembly2
-// tis-analyzer -val -val-profile analyzer assembly2.c -machdep x86_64 -gui
+// tis gui assembly2
 
 #include <stdint.h>
 #include <stdio.h>

advanced/flexible_array_member.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile interpreter flexible_array_member.c
+// tis gui flexible_array_member
 //
 // TrustInSoft Analyzer supports the C99 flexible array members syntax and the
 // zero-length array GNU extension, by checking accesses against the base only.

advanced/register.c

@@ -1,17 +1,17 @@
-// tis-analyzer -val -val-profile analyzer register.c
+// tis gui register
 // gcc register.c -o /dev/null
 
 #include <stdio.h>
 
 int main(void) {
-    // in C, register and auto are obsolete keywords, tis-analyzer ignores them
+    // in C, register and auto are obsolete keywords, the analyzer ignores them
     auto int x = 4;
     register int y = 5;
     int z = x + y;
 
     printf("z = %d\n", z);
 
-    // tis-analyzer does not detect these ; your compiler will
+    // the analyzer does not detect these ; your compiler will
     int *px = &x; // not necessarily legal
     int *py = &y; // never legal
 }

advanced/tis_address.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile analyzer tis_address.c
+// tis gui tis_address
 // With pointer -> int conversions, the analyzer will try its best to keep the
 // value precise
 

advanced/trustinsoft/config.json

@@ -0,0 +1,44 @@
+{
+  "common": {
+    "prefix_path": "..",
+    "val": true
+  },
+  "analyses": [
+    {
+      "name": "assembly1",
+      "files": [ "assembly1.c" ],
+      "val-profile": "analyzer"
+    },
+    {
+      "name": "assembly2",
+      "files": [ "assembly2.c" ],
+      "machdep": "x86_64",
+      "val-profile": "analyzer"
+    },
+    {
+      "name": "flexible_array_member",
+      "files": [ "flexible_array_member.c" ],
+      "val-profile": "interpreter"
+    },
+    {
+      "name": "register",
+      "files": [ "register.c" ],
+      "val-profile": "analyzer"
+    },
+    {
+      "name": "tis_address",
+      "files": [ "tis_address.c" ],
+      "val-profile": "analyzer"
+    },
+    {
+      "name": "variable_length_array",
+      "files": [ "variable_length_array.c" ],
+      "val-profile": "interpreter"
+    },
+    {
+      "name": "volatile",
+      "files": [ "volatile.c" ],
+      "val-profile": "analyzer"
+    }
+  ]
+}

advanced/variable_length_array.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile interpreter variable_length_array.c
+// tis gui variable_length_array
 
 void f(int size) {
     short v[size];

advanced/volatile.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile analyzer volatile.c
+// tis gui volatile
 //
 // Volatile variables are assumed to be always generalized, even after an
 // assignment. To control this behavior, use `-remove-volatile` or the Volatile

level1/invalid_pointer.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile interpreter invalid_pointer.c
+// tis gui invalid_pointer
 
 #include <stddef.h>
 #include <stdio.h>

level1/out_of_bounds.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile interpreter out_of_bounds.c
+// tis gui out_of_bounds
 // This a 1-char typo, could easily be missed in a code review.
 
 #include <stdio.h>

level1/signed_overflow.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile interpreter signed_overflow.c
+// tis gui signed_overflow
 
 #include <limits.h>
 #include <stdio.h>

level1/trustinsoft/config.json

@@ -0,0 +1,21 @@
+{
+  "common": {
+    "prefix_path": "..",
+    "val": true,
+    "val-profile": "interpreter"
+  },
+  "analyses": [
+    {
+      "name": "invalid_pointer",
+      "files": [ "invalid_pointer.c" ]
+    },
+    {
+      "name": "out_of_bounds",
+      "files": [ "out_of_bounds.c" ]
+    },
+    {
+      "name": "signed_overflow",
+      "files": [ "signed_overflow.c" ]
+    }
+  ]
+}

level2/0_introduction/0_unlikely_path.c

@@ -1,5 +1,6 @@
-// tis-analyzer -val -val-profile interpreter 0_unlikely_path.c
-// tis-analyzer -val -val-profile analyzer 0_unlikely_path.c
+// {
+//   "val-profile": "analyzer"
+// }
 
 #include <stdlib.h>
 

level2/0_introduction/1_tis_interval.c

@@ -1,4 +1,6 @@
-// tis-analyzer -val -val-profile analyzer 1_tis_interval.c
+// {
+//   "val-profile": "analyzer"
+// }
 
 #include <stdio.h>
 #include <tis_builtin.h>

level2/0_introduction/2_absolute.c

@@ -1,4 +1,6 @@
-// tis-analyzer -val -val-profile analyzer 2_absolute.c
+// {
+//   "val-profile": "analyzer"
+// }
 
 #include <limits.h>
 #include <tis_builtin.h>

level2/0_introduction/trustinsoft/config.json

@@ -0,0 +1,28 @@
+{
+  "common": {
+    "prefix_path": "..",
+    "val": true
+  },
+  "analyses": [
+    {
+      "name": "0_unlikely_path",
+      "files": [ "0_unlikely_path.c" ],
+      "val-profile": "interpreter"
+    },
+    {
+      "name": "0_unlikely_path",
+      "files": [ "0_unlikely_path.c" ],
+      "val-profile": "analyzer"
+    },
+    {
+      "name": "1_tis_interval",
+      "files": [ "1_tis_interval.c" ],
+      "val-profile": "analyzer"
+    },
+    {
+      "name": "2_absolute",
+      "files": [ "2_absolute.c" ],
+      "val-profile": "analyzer"
+    }
+  ]
+}

level2/1_slevel/0_is_zero.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile analyzer 0_is_zero.c
+// tis gui 0_is_zero
 // How to remove the false alarm?
 
 #include <stdio.h>

level2/1_slevel/1_init_buffer.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile analyzer 1_init_buffer.c
+// tis gui 1_init_buffer
 // How to remove the false alarm?
 
 #include <stdio.h>

level2/1_slevel/2_always_zero.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile analyzer 2_always_zero.c
+// tis gui 2_always_zero
 // How to remove the false alarm?
 #include <tis_builtin.h>
 

level2/1_slevel/3_loop.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile analyzer 3_loop.c 
+// tis gui 3_loop
 // How to remove the false alarms?
 #include <tis_builtin.h>
 
@@ -8,7 +8,7 @@ int main(void) {
     for (int i = 0; i < 30; i++) {
         if (tis_nondet(0, 1))
           a += 1 << i;
-        else                  
+        else
           b += 1 << i;
     }
     tis_show_each("", a, b);

level2/1_slevel/corrections/0_is_zero.c

@@ -1,4 +1,7 @@
-// tis-analyzer -val -val-profile analyzer 0_is_zero.c -slevel 2
+// {
+//   ..,
+//   "slevel": 2
+// }
 //
 // C code structures create multiple states naturally, raising the SLevel limit
 // allows these states to stay separated.

level2/1_slevel/corrections/1_init_buffer.c

@@ -1,7 +1,10 @@
-// tis-analyzer -val -val-profile analyzer 1_init_buffer.c -slevel 42
+// {
+//   ..,
+//   "slevel": 42
+// }
 //
 // The SLevel also describes how many turns of a loop are done precisely.
 //
 // Note that there is no impact with -slevel 1000000. Also note that there is no
-// alarm at -slevel 11: the first 11 turns of the loop are precise, which is 
+// alarm at -slevel 11: the first 11 turns of the loop are precise, which is
 // what we need.

level2/1_slevel/corrections/2_always_zero.c

@@ -1,4 +1,7 @@
-// tis-analyzer -val -val-profile analyzer corrections/2_always_zero.c -slevel 11
+// {
+//   ..,
+//   "slevel": 11
+// }
 //
 // Changes: tis_interval() -> tis_interval_split(), added SLevel.
 //

level2/1_slevel/corrections/3_loop.c

@@ -1,4 +1,7 @@
-// tis-analyzer -val -val-profile analyzer 3_loop.c -slevel 60
+// {
+//   ..,
+//   "slevel": 60
+// }
 //
 // `int tis_nondet(int a, int b)` is a built-in function of the analyzer. It
 // takes in two values, and returns two states: one where the return value is

level2/1_slevel/trustinsoft/config.json

@@ -0,0 +1,25 @@
+{
+  "common": {
+    "prefix_path": "..",
+    "val": true,
+    "val-profile": "analyzer"
+  },
+  "analyses": [
+    {
+      "name": "0_is_zero",
+      "files": [ "0_is_zero.c" ]
+    },
+    {
+      "name": "1_init_buffer",
+      "files": [ "1_init_buffer.c" ]
+    },
+    {
+      "name": "2_always_zero",
+      "files": [ "2_always_zero.c" ]
+    },
+    {
+      "name": "3_loop",
+      "files": [ "3_loop.c" ]
+    }
+  ]
+}

level2/2_fine_tuning/corrections/0_slow.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile analyzer corrections/0_slow.c
+// corrections/0_slow.c
 //
 // Changes: tis_interval() -> tis_interval_split(), slevel ACSL directive
 //

level2/2_fine_tuning/corrections/1_smart.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile analyzer corrections/1_smart.c
+// corrections/1_smart.c
 //
 // The analyzer splits the states on any condition: this includes ACSL
 // assertions. We isolate a 0 state that gets eliminated, all other values are

level2/2_fine_tuning/corrections/2_smarter.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile analyzer corrections/2_smarter.c
+// corrections/2_smarter.c
 //
 // The initial issue was about removing a value from the middle of an interval,
 // but the analyzer is capable of removing a value from the bounds of an

level2/2_fine_tuning/imprecise.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile analyzer imprecise.c
+// tis gui imprecise
 // Hot to get rid of the false alarm?
 
 #include <tis_builtin.h>

level2/2_fine_tuning/trustinsoft/config.json

@@ -0,0 +1,13 @@
+{
+  "common": {
+    "prefix_path": "..",
+    "val": true,
+    "val-profile": "analyzer"
+  },
+  "analyses": [
+    {
+      "name": "imprecise",
+      "files": [ "imprecise.c" ]
+    }
+  ]
+}

level2/3_val_split_return/0_is_zero.c

@@ -1,4 +1,4 @@
-// tis-analyzer -val -val-profile analyzer 0_is_zero.c -slevel-function f:10
+// tis gui 0_is_zero
 // How to remove the false alarm?
 
 #include <stdio.h>

level2/3_val_split_return/1_full_vs_auto.c

@@ -1,6 +1,6 @@
-// tis-analyzer -val -val-profile analyzer 1_full_vs_auto.c -slevel 100
-// tis-analyzer -val -val-profile analyzer 1_full_vs_auto.c -slevel 100 -val-split-return-function f:full
-// tis-analyzer -val -val-profile analyzer 1_full_vs_auto.c -slevel 100 -val-split-return-function f:auto
+// tis gui 1_full_vs_auto
+// tis gui 1_full_vs_auto_split_full
+// tis gui 1_full_vs_auto_split_auto
 //
 // The auto heuristic is based on data computed at the parsing phase.
 

level2/3_val_split_return/corrections/0_is_zero.c

@@ -1,4 +1,8 @@
-// tis-analyzer -val -val-profile analyzer 0_is_zero.c -slevel 10 -val-split-return-function f:full
+// {
+//   ..,
+//   "slevel": 10,
+//   "val-split-return-function": { "f":full }
+// }
 //
 // The strategy is changed for the callee, propagating more states in the
 // caller. Do not forget SLevel for the caller!

level2/3_val_split_return/trustinsoft/config.json

@@ -0,0 +1,37 @@
+{
+  "common": {
+    "prefix_path": "..",
+    "val": true,
+    "val-profile": "analyzer"
+  },
+  "analyses": [
+    {
+      "name": "0_is_zero",
+      "files": [ "0_is_zero.c" ],
+      "slevel-function": {
+        "f": 10
+      }
+    },
+    {
+      "name": "1_full_vs_auto",
+      "files": [ "1_full_vs_auto.c" ],
+      "slevel": 100
+    },
+    {
+      "name": "1_full_vs_auto_split_full",
+      "files": [ "1_full_vs_auto.c" ],
+      "slevel": 100,
+      "val-split-return-function": {
+        "f": "full"
+      }
+    },
+    {
+      "name": "1_full_vs_auto_split_auto",
+      "files": [ "1_full_vs_auto.c" ],
+      "slevel": 100,
+      "val-split-return-function": {
+        "f": "auto"
+      }
+    }
+  ]
+}