Frama-C: compiling on Cygwin / Windows 8.1

An easy question for those who compile C on windows! I want to use the latest version of the Frama-C C static analyzer and its GUI on windows 8. As far as I can tell, the most recent version that...

Launching Frama-c neon with jessie

I have installed frama-c and why3 but when i try to launch frama-c I get an error with jessie3. frama-c -verbose 2 [kernel] warning: cannot load plug-in `Jessie3' (incompatible with...

Calculate the range of an input which results in satisfying a predicate

Lets say we have the following C code: int my_main(int x){ if (x > 5){ x++; if (x > 8){ x++; if (x < 15){ //@(x >= 9 && x <= 14); } } } ...

How customize machine dependency in Frama-C?

I have got a 16-bit MPU which is different from x86_16 in size of size_t, ptrdiff_t etc. Can anybody give me details and clear instructions about how to customize machine dependency in Frama-C for my MPU?

Frama-c : Function calls and static variables

I'm currently discovering frama-c's features, and especially WP & Value's analysis tools. My final goal is to be able to use frama-c on larger codes that involves several layers with : a lot of...

Verification of function that sums array of int vs array of float using FramaC/WP

I am trying to specify and verify this simple function that sums up an array. This specification for an array of ints is accepted by WP: /*@ axiomatic Sum_Int { logic int sum_int(int...

Satisfying Proof Obligations for memcpy? [Frama-C]

We've been using Frama-C for 'experimental' static analysis on a commercial project (integrated into our CI, with a few selective blocking checks, on a small section of the overall codebase). One...

Coq file generated by WP does not compile

I have installed frama-c (18.0) and coqide (8.9) through opam (plus other needed dependencies of course, but that may not be the matter here). Well the point is I simply installed it through opam,...

How could I filter .csv generated by "report" plug-in in Frama-C?

Currently I'm executing: frama-c -wp -wp-rte -report-rules test_rules.json -wp-split -wp-fct max -wp-status-maybe -wp-status-invalid -wp-timeout 10 -wp-prover alt-ergo -wp-par 12...

Checking C code for invalid memory access with Frama-C

I am given this C code (the details of the code, including possible bugs, are not very relevant): int read_leb128(char **ptr, char *end) { int r = 0; int s = 0; char b; do { if...

Dynamic array with Frama-C and Eva

In https://stackoverflow.com/a/57116260/946226 I learned how to verify that a function foo that operates on a buffer (given by a begin and end pointer) really only reads form it, but creating a...

Syntax error when trying to use inductive predicate

I am trying to use the example of an inductive predicate taken from the webpage https://frama-c.com/acsl_tutorial_index.html: #include <stddef.h> #include <stdlib.h> typedef struct _list { int...

Problem of Non-Terminating Function (no dependencies)

Using Frama-C, I am trying to slice just one source code as follows: #include <stdio.h> #include <stdlib.h> #include <time.h> typedef struct { int event; int status; int*...

How verification of Shell sorting in ACSL Frama-C?

There is a software implementation of Shell sorting in C, and I also annotated it for verification in Frama-C. It is not possible to correctly compose invariants and prove the correctness of the...

ACSL proof of a function that checks if an array is sorted in increasing or decreasing order

I'm trying to prove the correctness of an function that checks if an array is sorted in increasing/decreasing order or not sorted. The behaviour is to return -1 if sorted in decreasing order, 1 if...

Verification of Shell Sorting algorithm loop invariants?

Good day to all! I wrote the Shell sort verification code, but I can’t build the correct loop invariants.It is not possible to correctly compose invariants and prove the correctness of the...

Formal proof of a recursive Quicksort using frama-c

As homework, I've decided to try verify an implementation of quicksort (taken and adapted from here) using frama-c with wp and rte plugins. Note that at first leftmost is 0 and rightmost is equal...

Proving the average value of an array

Hello I want to prove the computation of the average of all the values contained in a 1d array, so far I have the following program : #include <stdbool.h> typedef unsigned int size_t; typedef...

How to install Frama-C on Manjaro 18.1.5?

I'm trying to install frama-c on my distro of manjaro 18.1.5, but no matter what I try, I always have an error. First I tried to install via the AUR, and it seems to work, but when i try to open a...

What loop invariants to use for an integer logarithm?

As I am having my first steps in C formal verification with Frama-C, I am trying to formally verify an integer binary logarithm function written as follows: //@ logic integer pow2(integer n) = (n...

How do i analyse a complex project like open62541?

I am a student and currently trying to analyse the reference implementation for the OPC Ua protocol in C with cppcheck and frama-c. My goal is not to do very dedicated testing but more some...

Frama-C acsl max example from manual not working

I believe I am missing something obvious, but I have tried a lot and I haven't managed to find the source of the problem. I am following the acsl guide from Frama-C. There is this introductory...

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...

Verifying validity of pointer in frama-c

This is a really early frama-c question so sorry about that but I've been at it for a few hours and I can't get a really simple function to verify. I know it's complaining about the function...

error while installing gmp (frama-c prerequisite) on mac os catalina using opam on terminal

I ran these commands to install Frama-C as said on http://frama-c.com/install-sulfur-20171101.html#installing-frama-c-on-mac-os-x: brew install autoconf opam Do not forget to opam init and eval...

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; } ...

How do you tell Frama-C and Eva that an entry point's parameters are assumed valid?

Take the following C code example. struct foo_t { int bar; }; int my_entry_point(const struct foo_t *foo) { return foo->bar; } In our case, my_entry_point will be called from assembly,...

Frama-C's GUI (frama-c-gui) not installed despite installing frama-c on WSL Ubuntu

I followed the instructions on http://frama-c.com/install-21.1-Scandium.html#installing-frama-c-on-windows-via-wsl completely to install Frama-C (21.1) using opam. I want to use the GUI for...

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...

What should I do when this error occurs? Alt-Ergo: "Unknown error"

When I run the WP example, there is an error, and i don't know what it is. /*@ requires \valid(a) && \valid(b); @ ensures A: *a == \old(*b) ; @ ensures B: *b == \old(*a) ; @ assigns *a,*b...