Why3 is unable to run prover on windows via cygwin

I am trying to use cvc4 prover with Frama-c wp plugin through Why3 on Windows environment. I have frama-c and why3 installed on my system. Why3 is configured properly to include cvc4 as a prover...

The exact mechanism of mapping WhyML into SMT logic

Good day, auto deduction and verification hackers! In order to gain a deeper understanding of how exactly WhyML provides proofs for ACSL-annotated C programs I am trying to manually "reproduce"...

Using Okta IdP with an SP that uses dynamic ACSURL

We're in a situation where we are setting up an application to use Okta for SSO. The application is SAML 2.0 compliant, but it does send out an AssertionConsumerServiceURL that is dynamic (a...

Verification of a linear search with Frama-C

I'm yet again perplexed by a simple verification exercise, this time in Frama-C (Sodium) using the WP plugin, since I couldn't get Jessie to work on the uni workstations (in process of being...

ACSL - Can't prove function

I'm trying to prove this function, but in vain. I'm also using another function, but I proved it. Could anyone help me? I'm using Frama-C Sodium version with Alt-ergo 3 as prover. Given...

ACSL Bit String Flicking

I need help with an ACSL Problem. The contest was done in 2014-2015. It is just practice and I want to see if I did the problem correctly. Bit-String Flicking: Solve for x (5 bits) in the...

Need help on past acsl program from 2013

My teacher is making us do an old ACSL program for practice, and he said that we can use any resources we want. The program is from 2013. link here:...

Sorting a sentence using arrays and strings

Sorry guys forewarning I suck at coding but have a big project and need help! Input: A complete Sentence. Output: The sorted order (ASCii Chart Order) of the sentence (ignore case.) Output a...

What does the message "unreachable entry point" mean?

I have a file containing several ACSL assertions (file.c): #include <stdio.h> #include <stdlib.h> void foo() { int a=0; //@ assert(a==0); } void print(const char* text) { int a=0; ...

ACSL "assigns" annotation for inner structs and fields of C code

Suppose we have such a data structure: #typedef struct { int C_Field; }C; #typedef struct { C B_Array[MAX_SIZE]; }B; #typedef struct { B A_Array[MAX_SIZE]; }A; It seems that Frama-C...

Shall we write "assert" after each function call when a sequence of functions are called?

Let me start my question by this example: void A (void) { B(); C(); D(); E(); ... // function calls go on. return; } Now let's add ACSL annotations to the code: /*@ ensures...

ocamlfind: Package `lablgtk2.gnomecanvas' not found on ubuntu 17.04

I am trying to install Frama-C gui Phosphorus from repository (6aa64) on Ubuntu 17.04 (Zesty). Frama-C opam works fine but it lacks the GUI as far as I can tell + I might want to patch frama-C...

How do I debug ACSL in frama-c?

I'm trying to learn ACSL but am stumbling with trying to write a complete specification. My code #include <stdint.h> #include <stddef.h> #define NUM_ELEMS (8) /*@ requires expected != test; @...

How to force a memory location to be valid in ACSL?

I define device accesses as thus volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS; I've modeled the accesses using @ volatile dev->somereg reads somereg_read writes...

How to prove why3 generated script in coq?

I use frama-C WP and want to debug my ACSL annotations (to understand why provers say me "don't know"). I have some green or orange results. I open why3 IDE and see the generated scripts. Then I...

How to prove an iterative loop with computations in frama-c wp?

I have my test code (to study the WP loop invariants) which adds two long integers with each digit's representation in an array cell: int main(int argc, const char * argv[]) { char a[32],...

no module named gnuradio

I installed the UHD and GNU Radio on Ubuntu 16.4 based on instructions (https://kb.ettus.com/Building_and_Installing_the_USRP_Open-Source_Toolchain_(UHD_and_GNU_Radio)_on_Linux) I’m getting the...

Frama-C warning: Missing assigns clause (assigns 'everything' instead)

I'm testing this small program with frama-c and I keep getting the same error. I'm not sure what it means. I'm particularly confused on what assigns everything means. Here is the code in...

Unbounded function in EACSL Frama-C plugin

I am trying to generate contracts in C with E-ACSL plugin from FRAMA-C for the following program: struct lnode { int value; struct lnode *next; }; struct set { int capacity; int...

E-ACSL logic function call error - Unbound function

I want to define simple function contracts (defined in ACSL manual, section 2.3.2) from the program insert.c stated below. These contracts will be defined according to the observer functions (e.g:...

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

Equivalence between C/frama-c and Spark-ada

I'm studying the framework Frama-c, and I'm wondering if there is an equivalence between C/Frama-c and Spark Ada. I know that it can seem quite odd to compare such different languages, but after...

sh.exe is preventing windows cmd move command from working

I am running an old application called ACSLX. It is trying to call a DOS move command, but because sh.exe is in my path, I am getting an error. sh.exe is part of Git and also RTools, both of which...

How to validate code that read/write to hardware memory mapped registers (mmio) with frama-c Eva plugin or WP-RTE?

The closest answer I found maybe related to -absolute-valid-range for the Eva plugin but is that it? Do I have to come up with read/write ACSL predicates to do dummy read/write? Sample...

Frama-C order function

I am trying to prove the correctness of my sorting function 'order' with Frama-C with the ACSL language. I have an additional 'swap' function to permute two values of my array 't'. EDIT : I...

How do I prove code with a real axiomatic in Frama-C

I have changed the int type to float in the "Inner Product" code from the ACSL-by-Example book (the code with int type worked for me) and now I am not able to prove the loop invariant inner. I...

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

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

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

Relevant tags