release RPP v0.0.2

.gitignore

@@ -178,3 +178,6 @@ Makefile.plugin.generated
 /doc/Grammar/grammar.fdb_latexmk
 /doc/Grammar/grammar.fls
 /doc/Grammar/grammar.synctex.gz
+/rpp-manual.pdf
+/frama-c-rpp-*
+/LICENSE

Makefile

@@ -1,7 +1,7 @@
 ##########################################################################
 #  This file is part of RPP plug-in of Frama-C.                          #
 #                                                                        #
-#  Copyright (C) 2016-2018                                               #
+#  Copyright (C) 2016-2023                                               #
 #    CEA (Commissariat à l'énergie atomique et aux énergies              #
 #    alternatives)                                                       #
 #                                                                        #
@@ -18,6 +18,9 @@
 #  for more details (enclosed in the file LICENSE).                      #
 ##########################################################################
 
+VERSION = 0.0.2
+EXTRAVERSION ?=
+
 ifndef FRAMAC_SHARE
 FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
 endif
@@ -48,6 +51,15 @@ PLUGIN_TESTS_DIRS := rpp \
 
 include $(FRAMAC_SHARE)/Makefile.dynamic
 
+
+ifeq ("$(OPENSOURCE)","no")
+LICENSE=PROPRIETARY
+HEADERS=HEADERS_PROPRIETARY
+else
+LICENSE=LGPL
+HEADERS=HEADERS_LGPL
+endif
+
 RPP_DISTRIBUTED_FILES=rpp_options.ml rpp_options.mli \
 	rpp_extend_checker.ml rpp_extend_checker.mli \
 	rpp_parser.ml rpp_parser.mli \
@@ -58,12 +70,33 @@ RPP_DISTRIBUTED_FILES=rpp_options.ml rpp_options.mli \
 	rpp_predicate_visitor_axiom.ml rpp_predicate_visitor_axiom.mli \
 	rpp_core.ml rpp_core.mli \
 	rpp_register.ml rpp_register.mli \
-	rpp_gui.ml rpp_gui.mli \
-	Makefile
+	rpp_gui.ml rpp_gui.mli rpp_types.mli Rpp.mli \
+	Makefile rpp-manual.pdf README.md LICENSE opam
+
+NO_HEADERS=rpp-manual.pdf README.md LICENSE opam
 
+license:
+	cp $(LICENSE) LICENSE
 
-headers::
+rpp-manual.pdf:
+	make -C doc/Grammar
+	cp doc/Grammar/grammar.pdf $@
+
+headers:: license
 	$(PRINT_MAKING) $@
 	headache -c .headache_config.txt \
-                 -h .LICENSE \
-                 $(RPP_DISTRIBUTED_FILES)
+                 -h $(HEADERS) \
+                 $(filter-out $(NO_HEADERS), $(RPP_DISTRIBUTED_FILES))
+
+ifeq ("$(EXTRAVERSION)","")
+DISTRIBDIR=frama-c-rpp-$(VERSION)
+else
+DISTRIBDIR=frama-c-rpp-$(VERSION)-$(EXTRAVERSION)
+endif
+
+distrib: headers rpp-manual.pdf
+	$(RM) -r $(DISTRIBDIR)
+	$(RM) $(DISTRIBDIR).tar.gz
+	$(MKDIR) $(DISTRIBDIR)
+	tar -cf - $(RPP_DISTRIBUTED_FILES) | tar -C $(DISTRIBDIR) -xf -
+	tar zcf $(DISTRIBDIR).tar.gz $(DISTRIBDIR)

README.md

@@ -4,21 +4,37 @@ This is the *RPP (Relational Property Prover)* plug-in of *Frama-C*.
 
 ## Relational Properties
 
-Relational properties are properties invoking any finite number of function calls of possibly dissimilar functions with possible nested calls. Examples:
-
-       ∀ x1,x2; x1 < x2 ⇒ f(x1) < f(x2)
-
-       ∀ message, key; message = Decrypt(Encrypt(message,key),key)
-
+Relational properties are properties invoking any finite number of function calls
+of possibly dissimilar functions with possible nested calls. Examples:
+
+      ∀ x1,x2; x1 < x2 ⇒ f(x1) < f(x2)
+
+      ∀ message, key; message = Decrypt(Encrypt(message,key),key)
+
+      ∀ x1,x2; compare(x1,x2) == -compare(x2,x1);
+
+      ∀ x1,x2,x3; (compare(x1,x2) > 0 && compare(x2,x3) > 0) ==> compare(x1,x3) > 0;
+
+      ∀ x1,x2,x3; compare(x1,x2) == 0 ==> compare(x1,x3) == compare(x2,x3);
+
 
 ## A Relational Property Prover
 
-*RPP* is a *Frama-C* plug-in designed for the proof of relational properties. It is based on the technique of self-composition and works like a preprocessor for *WP* plug-in. After its execution on a project containing relational properties annotations, the proof on the generated code proceeds like any other proof with *WP*: proof obligations are generated and can be either discharged automatically by automatic theorem
-provers (e.g. *Alt-Ergo*, *CVC4*, *Z3*) or proven interactively (e.g. in *Coq*). The plug-in also generates an axiomatic definition and additional annotations that allow to use a relational property as a hypothesis for the proof of other properties in a completely automatic and transparent way.
+*RPP* is a *Frama-C* plug-in designed for the proof of relational properties.
+It is based on the technique of self-composition and works like a preprocessor
+for *WP* plug-in. After its execution on a project containing relational
+properties annotations, the proof on the generated code proceeds like any other
+proof with *WP*: proof obligations are generated and can be either discharged
+automatically by automatic theorem
+provers (e.g. *Alt-Ergo*, *CVC4*, *Z3*) or proven interactively (e.g. in *Coq*).
+The plug-in also generates an axiomatic definition and additional annotations
+that allow to use a relational property as a hypothesis for the proof of
+other properties in a completely automatic and transparent way.
 
 ## Installation
 
-*RPP v0.0.1* requires [Frama-C v17.0 Chlorine](https://frama-c.com/download.html). For more information see [Frama-C](http://frama-c.com).
+*RPP v0.0.1* requires [Frama-C v24.0 Chromium](https://frama-c.com/fc-versions/chromium.html).
+For more information see [Frama-C](http://frama-c.com).
 
 For installation, run following commands in the *RPP* directory:
 
@@ -35,7 +51,8 @@ For installation, run following commands in the *RPP* directory:
 
             frama-c-gui -rpp file.c
 
-- For graphic user interface (call from gui): select a relational clause in the gui, right click and select *RPP*. A new project will be generated ("RPP proof system").
+- For graphic user interface (call from gui): select a relational clause in the gui,
+right click and select *RPP*. A new project will be generated ("RPP proof system").
 
 - For generating only the self-composition transformation:
 
@@ -58,12 +75,21 @@ Concider function *f*:
 If we want to specify monotony on function *f* we can write:
 
 ```c
-         /*@ relational \forall int x1,x2; \callset(\call(f,x1,id1),\call(f,x2,id2)),x1 < x2 ==> \callresult(id1) < \callresult(id2);*/
+        int f(int x){
+            return x + 1;
+        }
+
+        /*@ relational \forall int x1,x2; \callset(\call(f,x1,id1),\call(f,x2,id2)),
+                                          x1 < x2 ==> \callresult(id1) < \callresult(id2);*/
 ```
 
 Or, because *f* has no side effect, we can also write a shorter form for pure functions:
 
 ```c
+        int f(int x){
+            return x + 1;
+        }
+
         /*@ relational \forall int x1,x2 ; x1 < x2 ==> \callpure(f,x1) < \callpure(f,x2);*/
 ```
 
@@ -80,12 +106,20 @@ If we now consider function *g* and global variable *y*:
 The specification of monotony on *g* can be written as follows:
 
 ```c
-       /*@ relational \callset(\call(f,id1),\call(f,id2)),\at(y,Pre_id1) < \at(y,Pre_id2) ==> \at(y,Post_id1) < \at(y,Post_id2);*/
+        int y;
+
+        int g(){
+            y = y + 1;
+        }
+
+        /*@ relational \callset(\call(f,id1),\call(f,id2)),
+                       \at(y,Pre_id1) < \at(y,Pre_id2) ==> \at(y,Post_id1) < \at(y,Post_id2);*/
 ```
 
 More examples are available in :
 
         test/rpp/
+        benchmarks/stackoverflow
 
 More documentations can be found in:
 

Rpp.mli

@@ -1,20 +1,20 @@
 (**************************************************************************)
 (*  This file is part of RPP plug-in of Frama-C.                          *)
 (*                                                                        *)
-(*  Copyright (C) 2016-2018                                               *)
-(*    CEA (Commissariat a l'energie atomique et aux energies              *)
-(*         alternatives)                                                  *)
+(*  Copyright (C) 2016-2023                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*    alternatives)                                                       *)
 (*                                                                        *)
 (*  you can redistribute it and/or modify it under the terms of the GNU   *)
 (*  Lesser General Public License as published by the Free Software       *)
-(*  Foundation, version 3.                                                *)
+(*  Foundation, version 2.1.                                              *)
 (*                                                                        *)
 (*  It is distributed in the hope that it will be useful,                 *)
 (*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
 (*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
 (*  GNU Lesser General Public License for more details.                   *)
 (*                                                                        *)
-(*  See the GNU Lesser General Public License version 3                   *)
-(*  for more details (enclosed in the file LICENCE).                      *)
-(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file LICENSE).                      *)
 (**************************************************************************)
+

benchmarks/stackoverflow/ArrayInt-false.c

@@ -16,9 +16,6 @@ struct AInt{
 /*@ requires 0 <= o1.length && o1.length < 1000;
   @ requires 0 <= o2.length && o2.length < 1000;
   @ assigns \result \from o1,o2;
-  @ relational \forall struct AInt x1,x2; \callpure(compare,x1,x2) == -(\callpure(compare,x2,x1));
-  @ relational \forall struct AInt x1,x2,x3; (\callpure(compare,x1,x2) > 0 && \callpure(compare,x2,x3) > 0) ==> \callpure(compare,x1,x3) > 0;
-  @ relational \forall struct AInt x1,x2,x3; \callpure(compare,x1,x2) == 0 ==> (\callpure(compare,x1,x3) == \callpure(compare,x2,x3));
 */
 int compare(struct AInt o1, struct AInt o2){
     int index, aentry, bentry;
@@ -39,3 +36,18 @@ int compare(struct AInt o1, struct AInt o2){
     }
     return 0;
   }
+
+/*@ relational
+      \forall struct AInt x1,x2;
+      \callpure(compare,x1,x2) == -(\callpure(compare,x2,x1));
+*/
+/*@ relational
+      \forall struct AInt x1,x2,x3;
+      (\callpure(compare,x1,x2) > 0 && \callpure(compare,x2,x3) > 0)
+      ==> \callpure(compare,x1,x3) > 0;
+*/
+/*@ relational
+      \forall struct AInt x1,x2,x3;
+      \callpure(compare,x1,x2) == 0 ==>
+      (\callpure(compare,x1,x3) == \callpure(compare,x2,x3));
+*/

benchmarks/stackoverflow/ArrayInt-true.c

@@ -16,9 +16,6 @@ struct AInt{
 /*@ requires 0 <= o1.length && o1.length < 1000;
   @ requires 0 <= o2.length && o2.length < 1000;
   @ assigns \result \from o1,o2;
-  @ relational \forall struct AInt x1,x2; \callpure(compare,x1,x2) == -(\callpure(compare,x2,x1));
-  @ relational \forall struct AInt x1,x2,x3; (\callpure(compare,x1,x2) > 0 && \callpure(compare,x2,x3) > 0) ==> \callpure(compare,x1,x3) > 0;
-  @ relational \forall struct AInt x1,x2,x3; \callpure(compare,x1,x2) == 0 ==> (\callpure(compare,x1,x3) == \callpure(compare,x2,x3));
 */
 int compare(struct AInt o1, struct AInt o2){
   int index, aentry, bentry;
@@ -45,3 +42,18 @@ int compare(struct AInt o1, struct AInt o2){
   }
   return 0;
 }
+
+/*@ relational
+      \forall struct AInt x1,x2;
+      \callpure(compare,x1,x2) == -(\callpure(compare,x2,x1));
+*/
+/*@ relational
+      \forall struct AInt x1,x2,x3;
+      (\callpure(compare,x1,x2) > 0 && \callpure(compare,x2,x3) > 0)
+      ==> \callpure(compare,x1,x3) > 0;
+*/
+/*@ relational
+      \forall struct AInt x1,x2,x3;
+      \callpure(compare,x1,x2) == 0 ==>
+      (\callpure(compare,x1,x3) == \callpure(compare,x2,x3));
+*/

benchmarks/stackoverflow/CatBPos-false.c

@@ -17,11 +17,7 @@ struct CatBPos{
   int getHdopBPosGetTimeIsNotVoid;
 };
 
-/*@ assigns \result \from x,y;
-  @ relational \forall int x1,x2; \callpure(IntCompare,x1,x2) == -(\callpure(IntCompare,x2,x1));
-  @ relational \forall int x1,x2,x3; (\callpure(IntCompare,x1,x2) > 0 && \callpure(IntCompare,x2,x3) > 0) ==> \callpure(IntCompare,x1,x3) > 0;
-  @ relational \forall int x1,x2,x3; \callpure(IntCompare,x1,x2) == 0 ==> (\callpure(IntCompare,x1,x3) == \callpure(IntCompare,x2,x3));
-*/
+/*@ assigns \result \from x,y; */
 int IntCompare(int x, int y){
   if (x < y){
     return -1;
@@ -33,11 +29,25 @@ int IntCompare(int x, int y){
   return 0;
 }
 
-/*@ assigns \result \from o1,o2;
-  @ relational \forall struct CatBPos x1,x2; \callpure(compare,x1,x2) == -(\callpure(compare,x2,x1));
-  @ relational \forall struct CatBPos x1,x2,x3; (\callpure(compare,x1,x2) > 0 && \callpure(compare,x2,x3) > 0) ==> \callpure(compare,x1,x3) > 0;
-  @ relational \forall struct CatBPos x1,x2,x3; \callpure(compare,x1,x2) == 0 ==> (\callpure(compare,x1,x3) == \callpure(compare,x2,x3));
+/*@ relational
+      \forall int x1,x2;
+      \callpure(IntCompare,x1,x2) == -(\callpure(IntCompare,x2,x1));
+*/
+
+/*@ relational
+      \forall int x1,x2,x3;
+      (\callpure(IntCompare,x1,x2) > 0 && \callpure(IntCompare,x2,x3) > 0)
+       ==> \callpure(IntCompare,x1,x3) > 0;
 */
+
+/*@ relational
+      \forall int x1,x2,x3;
+      \callpure(IntCompare,x1,x2) == 0 ==>
+      (\callpure(IntCompare,x1,x3) == \callpure(IntCompare,x2,x3));
+*/
+
+
+/*@ assigns \result \from o1,o2; */
 int compare(struct CatBPos o1, struct CatBPos o2) {
   int lCompare;
 
@@ -66,3 +76,20 @@ int compare(struct CatBPos o1, struct CatBPos o2) {
 
   return 0;
 }
+
+/*@ relational
+      \forall struct CatBPos x1,x2;
+      \callpure(compare,x1,x2) == -(\callpure(compare,x2,x1));
+*/
+
+/*@ relational
+      \forall struct CatBPos x1,x2,x3;
+      (\callpure(compare,x1,x2) > 0 && \callpure(compare,x2,x3) > 0)
+      ==> \callpure(compare,x1,x3) > 0;
+*/
+
+/*@ relational
+      \forall struct CatBPos x1,x2,x3;
+      \callpure(compare,x1,x2) == 0 ==>
+      (\callpure(compare,x1,x3) == \callpure(compare,x2,x3));
+*/

benchmarks/stackoverflow/Chromosome-false.c

@@ -15,10 +15,7 @@ struct Chromosome{
 
 /*@ requires o1.isNull != 0;
   @ assigns \result \from o1,o2;
-  @ relational \forall struct Chromosome x1,x2; \callpure(compare,x1,x2) == -(\callpure(compare,x2,x1));
-  @ relational \forall struct Chromosome x1,x2,x3; (\callpure(compare,x1,x2) > 0 && \callpure(compare,x2,x3) > 0) ==> \callpure(compare,x1,x3) > 0;
-  @ relational \forall struct Chromosome x1,x2,x3; \callpure(compare,x1,x2) == 0 ==> (\callpure(compare,x1,x3) == \callpure(compare,x2,x3));
-  */
+*/
 int compare(struct Chromosome o1, struct Chromosome o2) {
   if(o2.isNull == 0)
     return(1);
@@ -35,3 +32,19 @@ int compare(struct Chromosome o1, struct Chromosome o2) {
   else
     return(-1);
 }
+
+/*@ relational
+      \forall struct Chromosome x1,x2;
+      \callpure(compare,x1,x2) == -(\callpure(compare,x2,x1));
+*/
+/*@ relational
+      \forall struct Chromosome x1,x2,x3;
+      (\callpure(compare,x1,x2) > 0 && \callpure(compare,x2,x3) > 0)
+      ==> \callpure(compare,x1,x3) > 0;
+*/
+
+/*@ relational
+      \forall struct Chromosome x1,x2,x3;
+      \callpure(compare,x1,x2) == 0 ==>
+      (\callpure(compare,x1,x3) == \callpure(compare,x2,x3));
+  */

benchmarks/stackoverflow/Chromosome-true.c

@@ -29,10 +29,7 @@ int IntCompare(int x, int y){
 
 /*@ requires o1.isNull != 0;
   @ assigns \result \from o1,o2;
-  @ relational \forall struct Chromosome x1,x2; \callpure(compare,x1,x2) == -(\callpure(compare,x2,x1));
-  @ relational \forall struct Chromosome x1,x2,x3; (\callpure(compare,x1,x2) > 0 && \callpure(compare,x2,x3) > 0) ==> \callpure(compare,x1,x3) > 0;
-  @ relational \forall struct Chromosome x1,x2,x3; \callpure(compare,x1,x2) == 0 ==> (\callpure(compare,x1,x3) == \callpure(compare,x2,x3));
-  */
+*/
 int compare(struct Chromosome o1, struct Chromosome o2) {
     if(o2.isNull == 0)
 	return(1);
@@ -50,3 +47,20 @@ int compare(struct Chromosome o1, struct Chromosome o2) {
 
     return 0;
 }
+
+/*@ relational
+      \forall struct Chromosome x1,x2;
+      \callpure(compare,x1,x2) == -(\callpure(compare,x2,x1));
+*/
+
+/*@ relational
+      \forall struct Chromosome x1,x2,x3;
+      (\callpure(compare,x1,x2) > 0 && \callpure(compare,x2,x3) > 0)
+      ==> \callpure(compare,x1,x3) > 0;
+*/
+
+/*@ relational
+      \forall struct Chromosome x1,x2,x3;
+      \callpure(compare,x1,x2) == 0 ==>
+      (\callpure(compare,x1,x3) == \callpure(compare,x2,x3));
+  */