Skip to content

Stevendeo/CaFE

master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
***********               ******               ***********       ***********
***********              ********              ***********       ***********
**                      ***    ***             **                **
**                     ***      ***            **                **           
**                    ***        ***           ***********       ***********  
**                   ****************          ***********       ***********  
**                  ******************         **                **           
**                 ***              ***        **                **           
***********       ***                ***       **                ***********
***********      ***                  ***      **                ***********



A Frama-C model-checker.

********************************************************************************

INSTALLATION

See INSTALL

********************************************************************************

USAGE

Simply type "frama-c -cafe your_prog.c -cafe-formula your_spec.caret"

Here is a sample of currently available options.

-atom-simp          when on (on by default), tries to delete
                    self-inconsistent atoms. Uses CVC3. (set by default,
                    opposite option is -no-atom-simp)
-cafe               when on (off by default), model checking with CaRet
                    formulas (opposite option is -no-cafe)
-cafe-assert        when on (on by default), considers loop invariants as
                    true (set by default, opposite option is -cafe-no-assert)
-cafe-atoms         generates a file containing the atoms of the formula
                    (opposite option is -cafe-no-atoms)
-cafe-atoms-output <output-file>  file where the set of atoms from the
                    formula is output (default : console)
-cafe-auto          when on (on by default), generates the automaton.
                    Desactivate only for debug (set by default, opposite
                    option is -cafe-no-auto)
-cafe-closure       generates a file containing the closure set of the
                    formula in argument (opposite option is -cafe-no-closure)
-cafe-closure-output <output-file>  file where the formula closure is output
                    (default : console)
-cafe-dot           when on (off by default), generates the dot
                    representation of the automaton. When off, generates some
                    informations about the automaton. (opposite option is
                    -cafe-no-dot)
-cafe-dot-output <output-file>  file where the automaton, as a dot file, is
                    output (default : console)
-cafe-end           when on (on by default), considers the c program ends
                    eventually in any case. (set by default, opposite option
                    is -cafe-no-end)
-cafe-formula <caret-formula>  file in which the formula is written.
-cafe-main          when on (on by default), only checks the first loop
                    encourntered in the main.c file. Infinite paths on other
                    functions are not considered. (set by default, opposite
                    option is -cafe-no-main)
-cafe-output <output-file>  file where the result is output (default :
                    console)
-cafe-simp-level <n>  level of simplification : 0 for nothing ; 1 for
                    deleting unreachable states ; 2 for deleting dead-end
                    states ; 3 for complete simplification (2 by default) 
-cafe-states <output-file>  in this file will be found every information
                    about each state
-cafe-unr           when on (on by default),considers value is right when it
                    says a state is unreachable.  (opposite option is
                    -cafe-no-unr)
-fignore <<f1;...>>  List of the functions ignored by the analysis

********************************************************************************
Specification semantics

Specifications are written in the temporal logic CaRet (see "A temporal logic of nested calls and returns" or "Au temps en emporte le C" for details) 

Operators: 
{p} (an ACSL property. Always between brackets)
X(p) (next state, p holds)
(p) U (q) (p holds until q does)
F (p) (= true U p)
G (p) (= not (F (not p))) 

Tags:
In CaRet, operators have tags refering to the trace they are studying: 
"@N" : the usual execution path
"@A" : the abstract execution path, i.e. when a function is encountered, it skips it and goes to the return
"@P" : the past execution path, i.e. the previous nested call.

For example : 
    G@A({x > 0}) <=> 
    	   At any statement of the main function, x > 0 holds.
    G@N({p} => X@A(X@P {q})) <=> 
    	  Whenever p holds, then q must have hold at the previous nested call. 

About

A prototype of model-checker

Resources

License

LGPL-2.1, GPL-3.0 licenses found

Licenses found

LGPL-2.1
LICENCE
GPL-3.0
LICENSE

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published