Stack Overflow
Stack Overflow

Questions tagged [frama-c]

Frama-C is an Open Source suite of tools dedicated to the analysis of C source code.

Frama-C offers ready-to-use analyses for C programs: call graph, value analysis, functional dependencies, Program Dependence Graph, runtime monitoring, etc. It also allows the verification of functional properties, temporal logic, and much more. Results can be expressed in plain text, in SARIF, or in Frama-C's graphical interface.

Each analysis is implemented as a plug-in, and plug-ins inside the platform can use the results of one another. Frama-C is Open Source and extensible: new analyses can be implemented in OCaml as additional plug-ins that take advantage of existing ones. They communicate using the ACSL specification language, which also enables describing what the program is supposed to do.

Most provided analyses in Frama-C are sound: used within a delimited perimeter, all the behaviors that can happen at run-time are included in the behaviors statically predicted by Frama-C. Notwithstanding the possibility of bugs, plug-ins must be used as documented for the property to hold. This makes it possible to use Frama-C for the formal verification of C programs.

447 questions
6
votes
1 answer

How to prove the functionality of a C stringCompare function with Frama-C?

I would like to express, with Frama-c and the WP plug-in, that the stringCompare function written below acts as "it is supposed to" - namely: That given identical input strings, the function returns 0 and a result different from 0 if the strings are…
BHM
  • 63
  • 3
6
votes
1 answer

User Error: Prover 'alt-ergo' not found in why3.conf

I am trying to test a function with Frama-c: /*@ ensures \result >= x && \result >= y; ensures \result == x || \result == y; */ int max( int x, int y){ return (x>y) ? x : y; } After I installed all the requirements: OPAM, why3,…
I. Ali
  • 171
  • 2
  • 5
6
votes
1 answer

Calculate reachability to a function using frama-c's value analysis

Here is my example: int in; int sum(int n){ int log_input = n; int log_global = in; return 0; } int main(){ int n = Frama_C_interval(-10, 10); in = n; if (n > 0){ sum(n + 4); } return 0; } What I'd like to…
Maor Veitsman
  • 1,544
  • 9
  • 21
6
votes
2 answers

Can frama-c be used for header file analysis?

I was looking at frama-c as a way to process C header files in OCaml (e.g. for generating language bindings). It's attractive because it seems like a very well-documented and maintained project. However, after a lot of googling and searching through…
Martin DeMello
  • 11,876
  • 7
  • 49
  • 64
5
votes
1 answer

Why does the dependence graph of this scanf()-using program by Frama-C look like this?

I use the Frama-C tool to generate the dependence graph of this program(main.c). #include int main() { int n,i,m,j; while(scanf("%d",&n)!=EOF) { m=n; for(i=n-1;i>=1;i--) …
user1283336
  • 297
  • 3
  • 8
5
votes
1 answer

Frama-C Windows Binary Available?

I am looking to do some experimenting with the Frama-C open source project and would like to install the tools on a Windows 7 machine. It looks like previous versions have binary installers for Windows, but the latest version, Nitrogen, only has…
Bryan C.
  • 347
  • 1
  • 12
5
votes
1 answer

Static Analysis erroneously reports out of bounds access

While reviewing a codebase, I came upon a particular piece of code that triggered a warning regarding an "out of bounds access". After looking at the code, I could not see a way for the reported access to happen - and tried to minimize the code to…
ttsiodras
  • 10,602
  • 6
  • 55
  • 71
5
votes
2 answers

How does one prove simple equalities of non-deterministic values in Frama-C + EVA?

I'm a bit confused by the behavior of Frama-C version 18.0 (Argon). Given the following program: #include #include /*@ requires order: min <= max; assigns \result \from min, max; ensures result_bounded: min <= \result…
cody
  • 235
  • 1
  • 9
5
votes
1 answer

What is the meaning and purpose of "after" column in Frama-C EVA plugin

In the EVA tutorial, I found this screenshot: with an explanation:" The exact value that caused this is shown in column c5: -1. The C standard considers the left-shift of a negative number as undefined behavior. Because -1 is the only possible…
Thuy Nguyen
  • 353
  • 2
  • 10
5
votes
1 answer

How to link .cma files to my own Frama_C plugin?

I created my own Frama-C plugin by following the instructions of the Frama-C Development Guide (https://frama-c.com/download/frama-c-plugin-development-guide.pdf). However, I need to use the Mutex module provided by the Ocaml manual…
Gifi
  • 53
  • 4
5
votes
1 answer

Frama-c Magnesium : Unable to execute WP plugin on Windows

I installed frama-c Magnesium version using instruction provided here. I didn't get any error during installation and executing command frama-c -versionin Cygwin printed Frama-c version as: Magnesium-20151002. But when I executed -wp plugin on a…
Gunjan Aggarwal
  • 710
  • 5
  • 19
5
votes
1 answer

Use Frama-c to analyze a project with CMake build infrastructure

I need to use frama-c value analysis plug-in to analyze some projects. These projects use CMake build infrastructure as their build system. I have used frama-c to analyze each file separately. This way, the information about the entry point will be…
Mehrnoosh EP
  • 161
  • 7
5
votes
1 answer

How to use functions in Value.Eval_expr, Value.Eval_op etc modules of Frama-c Value plugin

I am trying to create a frama-c plugin. This plugin depends upon Frama-c Value plugin. I want to obtain and print value set of all the lvalue(s) in a C source code. In order to do that I want to use functions available in Value.Eval_exprs,…
Gunjan Aggarwal
  • 710
  • 5
  • 19
5
votes
1 answer

Assigns clause for local variables in Frama-C

I am trying to verify the following piece of code using frama-c /*@ ensures \result != \null; @ assigns \nothing; @*/ extern int *new_value(); //@ assigns *p; void f(int* p){ *p = 8; } //@ assigns \nothing; int main(void){ int *p =…
kruk
  • 137
  • 5
5
votes
0 answers

Handling dynamic allocation in Frama-C

I am trying to use Frama-C to verify safety properties of C code that includes dynamic memory allocation. The current version of the ACSL specification language (1.8) seems to be able to express a lot about dynamically allocated memory. However,…
Filip Nikšić
  • 151
  • 1
  • 4
1
2 3
…
29 30