Merge branch 'kostyantyn/bugfix/precond' into 'master'

Remove precond option from --rte flag of e-acsl-gss.sh

See merge request !118

src/plugins/e-acsl/doc/Changelog

@@ -15,6 +15,7 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2017/03/03] Remove precond rte option from e-acsl-gss.sh
 -* E-ACSL       [2017/03/02] Fix bts #1740 about incorrect monitoring of
 	        memory properties when early exiting a block through
 	        goto, break or continue.

src/plugins/e-acsl/man/e-acsl-gcc.sh.1

@@ -132,7 +132,6 @@ Valid arguments are:
   \fImem\fP               \- pointer or array accesses.
   \fIfloat-to-int\fP      \- casts from floating-point to integer.
   \fIdiv\fP               \- division by zero.
-  \fIprecond\fP           \- function calls based on contracts.
   \fIshift\fP             \- left and right shifts by a value out of bounds.
   \fpointer-call\fP       \- annotate functions calls through pointers.
   \fIall\fP               \- all of the above.

src/plugins/e-acsl/scripts/e-acsl-gcc.sh

@@ -97,8 +97,11 @@ rte_options() {
   local fc_options="signed-overflow unsigned-overflow \
     signed-downcast unsigned-downcast"
   # RTE assertions
-  local rte_options="div float-to-int mem pointer-call precond shift  \
+  local rte_options="div float-to-int mem pointer-call shift \
     trivial-annotations"
+  # Option supported by RTE but unsupported in E-ACSL, should
+  # always be negated
+  local rte_options_unsupported="precond"
   local generated="-rte" # Generated Frama-C options
 
   # Clean-up option strings
@@ -130,7 +133,7 @@ rte_options() {
     done
 
     # Generate assertion options for RTE (i.e., -rte-* or -rte-no-*)
-    for opt in $rte_options; do
+    for opt in $rte_options $rte_options_unsupported; do
       has_token $opt $asserts && prefix="-rte" || prefix="-rte-no"
       generated="$generated $prefix-$opt"
     done