2021-01-22 20:05 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001004Frama-CPlug-in > jessiepublic2013-03-27 09:44
Reporterboris 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001004: Jessie reports syntax error in .mlw file
DescriptionInvoking frama-c -jessie -pp-annot cc.c on the attached file produces:

Error while reading file '../cc.mlw':
File "cc/../cc.mlw", line 4342, characters 10-13:
syntax error
make: *** [why3ml] Error 1
[jessie] user error: Jessie subprocess failed: make -f cc.makefile why3ml

This file did verify with the previous version of Frama-C/Jessie/alt-ergo+simplify.
TagsNo tags attached.
Attached Files
  • c file icon cc.c (12,157 bytes) 2011-10-27 17:10 -
    #define false 0
    #define true 1
    typedef int bool;
    
    #define pre(...) \at(__VA_ARGS__,P)
    #define here(...) \at(__VA_ARGS__,H)
    #define unchanged(x,y) (pre(x) == here(x) && pre(y) == here(y))
    #define returns(x) assigns x; ensures \result == (x)
    
    
    
    /********** tempomat_lever **********/
    
    typedef enum {no_key, off, acc1, acc10, dec1, dec10, resume} tempomat_lever_t;
    
    tempomat_lever_t tempomat_lever_port;
    tempomat_lever_t tempomat_lever_previous_value = no_key;
    
    /*@ predicate tempomat_lever_get_spec{P,H}(tempomat_lever_t result) = here(
    		(pre(tempomat_lever_port != tempomat_lever_previous_value)  ==>  result == tempomat_lever_port) &&
    		(pre(tempomat_lever_port == tempomat_lever_previous_value)  ==>  result == no_key));
    */
    /*@	ensures tempomat_lever_get_spec{Pre,Here}(\result);
    */
    tempomat_lever_t tempomat_lever_get()
    {
    	tempomat_lever_t result;
    	tempomat_lever_t val = tempomat_lever_port;
    
    	if(val != tempomat_lever_previous_value) {
    		tempomat_lever_previous_value = val;
    		return val;
    	}
    	else return no_key;
    }
    
    
    
    /********** sensor **********/
    
    typedef int speed_t;
    typedef int accelerator_position_t;
    
    //@ ghost speed_t sensor_speed_result;
    /*@ returns(sensor_speed_result);
    	ensures 0 <= \result <= 250;
    */
    speed_t sensor_speed();
    
    //@ ghost bool sensor_brake_pedal_pressed_result;
    //@ returns(sensor_brake_pedal_pressed_result);
    bool sensor_brake_pedal_pressed();
    
    //@ ghost bool sensor_engine_rpm_low_result;
    //@ returns(sensor_engine_rpm_low_result);
    bool sensor_engine_rpm_low();
    
    bool sensor_driver_input_accelerate();
    
    accelerator_position_t sensor_accelerator_position();
    
    /********** tempomat **********/
    
    typedef struct {
    	bool active;
    	bool temp_override;
    	bool previously_active;
    	speed_t target_speed;
    	#define tempomat_min_speed 30
    	#define tempomat_max_speed 250
    } tempomat_t;
    
    
    //@ ghost speed_t tempomat_previous_speed;
    /*@ predicate tempomat_speed_range(integer speed) =
    		tempomat_min_speed <= speed <= tempomat_max_speed;
    	predicate tempomat_inv_speed(tempomat_t* this) =
    		this->active || this->previously_active  ==>  tempomat_speed_range(this->target_speed);
    	predicate tempomat_inv_prev_speed(tempomat_t* this) =
    		!this->active && this->previously_active  ==>  tempomat_previous_speed == this->target_speed;
    	predicate tempomat_inv0(tempomat_t* this) =
    		tempomat_inv_speed(this) && tempomat_inv_prev_speed(this);
    	predicate tempomat_active_no_temp_override(tempomat_t* this) =
    		this->active && !this->temp_override;
    */
    #define tempomat_inv_init	requires \valid(this);\
    							ensures tempomat_inv0(this);
    #define tempomat_inv		requires tempomat_inv0(this);\
    							tempomat_inv_init
    
    
    /*@	tempomat_inv_init
    */
    void tempomat_init(tempomat_t* this)
    {
    	this->active = false;
    	this->previously_active = false;
    }
    
    /*@ predicate tempomat_set_spec{P,H}(tempomat_t* this, integer speed) =
    		( tempomat_speed_range(speed)  ==>  here(this->active && this->target_speed == speed)) &&
    		(!tempomat_speed_range(speed)  ==>  (unchanged(this->active, this->target_speed)));
    */
    /*@	tempomat_inv
    	ensures tempomat_set_spec{Pre,Here}(this, speed);
    */
    void tempomat_set(tempomat_t* this, speed_t speed)
    {
    	if(tempomat_min_speed <= speed && speed <= tempomat_max_speed) {
    		this->active = true;
    		this->temp_override = false;
    		this->target_speed = speed;
    	}
    }
    
    /*@ predicate tempomat_deactivate_spec(tempomat_t* this) =
    		!this->active;
    */
    /*@	requires this->active;
    	tempomat_inv
    	ensures tempomat_deactivate_spec(this);
    */
    void tempomat_deactivate(tempomat_t* this)
    {
    	this->active = false;
    	this->temp_override = false;
    	this->previously_active = true;
    	//@ ghost tempomat_previous_speed = this->target_speed;
    }
    
    
    //@ ghost speed_t tempomat_resume_speed;
    /*@ predicate tempomat_resume_spec{P,H}(tempomat_t* this) = here(
    		(pre( this->previously_active) ==> this->active && this->target_speed == tempomat_previous_speed) &&
    		(pre(!this->previously_active) ==> tempomat_set_spec{P,H}(this, tempomat_resume_speed)));
    */
    /*@	requires !this->active;
        tempomat_inv
    	ensures tempomat_resume_spec{Pre,Here}(this);
    */
    void tempomat_resume(tempomat_t* this)
    {
    	if(this->previously_active) this->active = true;
    	else {
    		tempomat_set(this, sensor_speed());
    		//@ ghost tempomat_resume_speed = sensor_speed_result;
    	}
    }
    
    
    /*@ predicate tempomat_change_speed_spec{P,H}(tempomat_t* this, integer delta) =
    		tempomat_set_spec{P,H}(this, pre(this->target_speed) + delta);
    */
    /*@	requires -20 <= delta <= 20;
    	requires this->active;
        tempomat_inv
        ensures tempomat_change_speed_spec{Pre,Here}(this, delta);
    */
    void tempomat_change_speed(tempomat_t* this, speed_t delta)
    {
    	tempomat_set(this, this->target_speed + delta);
    }
    
    
    //@ ghost tempomat_lever_t tempomat_handler_button;
    //@ ghost speed_t tempomat_handler_speed;
    //@ ghost bool tempomat_handler_brake_pedal_pressed;
    //@ ghost bool tempomat_handler_engine_rpm_low;
    //@ ghost bool tempomat_handler_driver_input_accelerate;
    
    /*@ predicate deactivation_event =
    		tempomat_handler_button == off ||
    		tempomat_handler_brake_pedal_pressed ||
    		tempomat_handler_engine_rpm_low ||
    		(tempomat_handler_speed < tempomat_min_speed);
    */
    /*@ predicate tempomat_handler_spec{P,H}(tempomat_t* this) = here(
    		tempomat_lever_get_spec{P,H}(tempomat_handler_button) &&
    		(deactivation_event && pre(!deactivation_event)  ==>  tempomat_deactivate_spec(this)) &&
    		(pre(this->active)  ==>  (
    			(!deactivation_event  ==>  (
    				(tempomat_handler_button == acc1  ==>  tempomat_change_speed_spec{P,H}(this, 1))  &&
    				(tempomat_handler_button == acc10  ==>  tempomat_change_speed_spec{P,H}(this, 10))  &&
    				(tempomat_handler_button == dec1  ==>  tempomat_change_speed_spec{P,H}(this, -1))  &&
    				(tempomat_handler_button == dec10  ==>  tempomat_change_speed_spec{P,H}(this, -10)) &&
    				this->active
    			)) &&
    			(tempomat_handler_driver_input_accelerate  ==>  !tempomat_active_no_temp_override(this))
    		)) &&
    		(pre(!this->active)  ==>  (
    			(tempomat_handler_button == acc1 || tempomat_handler_button == acc10 ||
    				tempomat_handler_button == dec1 || tempomat_handler_button == dec10  ==>
    				tempomat_set_spec{P,H}(this, tempomat_handler_speed)
    			) &&
    			(tempomat_handler_button == resume  ==>  tempomat_resume_spec{P,H}(this)) &&
    			(tempomat_handler_button != acc1 && tempomat_handler_button != acc10 &&
    				tempomat_handler_button != dec1 && tempomat_handler_button != dec10 &&
    				tempomat_handler_button != resume ==>  !this->active)
    		)));
    */
    /*@	tempomat_inv
    	ensures tempomat_handler_spec{Pre,Here}(this);
    */
    void tempomat_handler(tempomat_t* this)
    {
    	tempomat_lever_t button = tempomat_lever_get();
    	//@ ghost tempomat_handler_button = button;
    
    	if(this->active) {
    		switch(button) {
    			case acc1: tempomat_change_speed(this, 1); break;
    			case acc10: tempomat_change_speed(this, 10); break;
    			case dec1: tempomat_change_speed(this, -1); break;
    			case dec10: tempomat_change_speed(this, -10); break;
    			default: /* no action*/ break;
    		}
    		this->temp_override = sensor_driver_input_accelerate();
    		//@ ghost tempomat_handler_driver_input_accelerate = this->temp_override;
    		//@ assert tempomat_handler_driver_input_accelerate  ==>  !tempomat_active_no_temp_override(this);
    		if(button == off || sensor_brake_pedal_pressed() || sensor_engine_rpm_low() || sensor_speed() < tempomat_min_speed) {
    			//@ ghost tempomat_handler_brake_pedal_pressed = sensor_brake_pedal_pressed_result;
    			//@ ghost tempomat_handler_engine_rpm_low = sensor_engine_rpm_low_result;
    			//@ ghost tempomat_handler_speed = sensor_speed_result;
    			tempomat_deactivate(this);
    			//@ assert !tempomat_active_no_temp_override(this);
    		}
    	}
    	else {
    		switch(button) {
    			case acc1:
    			case acc10:
    			case dec1:
    			case dec10:
    				tempomat_set(this, sensor_speed());
    				//@ ghost tempomat_handler_speed = sensor_speed_result;
    				break;
    			case resume: tempomat_resume(this); break;
    			default: /* no action*/ break;
    		}
    	}
    }
    
    
    
    /********** electronic power control **********/
    
    //@ ghost typedef enum {tempomat, accelerator} epc_input_mode_t;
    //@ ghost epc_input_mode_t epc_input_mode;
    
    
    /*@ assigns epc_input_mode;
    	ensures epc_input_mode == tempomat;
    */
    void epc_input_tempomat(speed_t error);
    
    
    /*@ assigns epc_input_mode;
    	ensures epc_input_mode == accelerator;
    */
    void epc_input_manual(accelerator_position_t ap);
    
    
    /********** speed_controller **********/
    
    typedef struct {
    	tempomat_t tempomat;
    } speed_controller_t;
    
    
    /*@ predicate speed_controller_inv0(speed_controller_t* this) =
    		tempomat_inv0(&this->tempomat);
    */
    #define speed_controller_inv_init	requires \valid(this) && \valid(&this->tempomat);\
    									ensures speed_controller_inv0(this);
    #define speed_controller_inv		requires speed_controller_inv0(this);\
    									speed_controller_inv_init
    
    
    /*@	speed_controller_inv_init
    */
    void speed_controller_init(speed_controller_t* this)
    {
    	tempomat_init(&this->tempomat);
    }
    
    
    /*@ predicate speed_controller_run_spec{P,H}(speed_controller_t* this) = here(
    		tempomat_handler_spec{P,H}(&this->tempomat) &&
    		( tempomat_active_no_temp_override(&this->tempomat)  ==>  epc_input_mode == tempomat) &&
    		(!tempomat_active_no_temp_override(&this->tempomat)  ==>  epc_input_mode == accelerator));
    */
    /*@	speed_controller_inv
    	ensures speed_controller_run_spec{Pre,Here}(this);
    */
    void speed_controller_run(speed_controller_t* this)
    {
    	tempomat_handler(&this->tempomat);
    	if((&this->tempomat)->active && !(&this->tempomat)->temp_override) {
    		//@ assert tempomat_speed_range((&this->tempomat)->target_speed);
    		epc_input_tempomat((&this->tempomat)->target_speed - sensor_speed());
    	}
    	else {
    		epc_input_manual(sensor_accelerator_position());
    	}
    }
    
    
    
    /********** verification **********/
    
    /*@ speed_controller_inv
    	behavior acc_dec: assumes (&this->tempomat)->active;
    		ensures !deactivation_event  ==>
    			(button == acc1  ==>  tempomat_change_speed_spec{Pre,Here}(&this->tempomat, 1)) &&
    			(button == acc10  ==>  tempomat_change_speed_spec{Pre,Here}(&this->tempomat, 10)) &&
    			(button == dec1  ==>  tempomat_change_speed_spec{Pre,Here}(&this->tempomat, -1)) &&
    			(button == dec10  ==>  tempomat_change_speed_spec{Pre,Here}(&this->tempomat, -10));
    	behavior set: assumes !(&this->tempomat)->active;
     		ensures button == acc1 || button == acc10 || button == dec1 || button == dec10  ==>
    				tempomat_set_spec{Pre,Here}(&this->tempomat, tempomat_handler_speed);
    	behavior set_resume: assumes !(&this->tempomat)->active && !(&this->tempomat)->previously_active;
     		ensures button == resume  ==>  tempomat_set_spec{Pre,Here}(&this->tempomat, tempomat_resume_speed);
    	behavior resume: assumes !(&this->tempomat)->active && (&this->tempomat)->previously_active;
     		ensures button == resume  ==>  (&this->tempomat)->active && (&this->tempomat)->target_speed == tempomat_previous_speed;
     	behavior off: assumes button == off;
    		ensures deactivation_event;
     	behavior remains_off: assumes !(&this->tempomat)->active;
    		ensures button != acc1 && button != acc10 && button != dec1 && button != dec10 && button != resume  ==>
    		!(&this->tempomat)->active;
     	behavior remains_on: assumes (&this->tempomat)->active;
    		ensures !deactivation_event  ==>  (&this->tempomat)->active;
    */
    void speed_controller_verify_tempomat_lever_actions(speed_controller_t* this, tempomat_lever_t button)
    {
    	tempomat_lever_previous_value = no_key;
    	tempomat_lever_port = button;
    	speed_controller_run(this);
    }
    
    
    /*@ speed_controller_inv
    	behavior deactivate: assumes !deactivation_event;
    		ensures deactivation_event  ==>  !(&this->tempomat)->active;
    */
    void speed_controller_verify_deactivation(speed_controller_t* this)
    {
    	speed_controller_run(this);
    }
    
    
    /*@ speed_controller_inv
    	ensures  tempomat_active_no_temp_override(&this->tempomat)  ==>  epc_input_mode == tempomat;
    	ensures !tempomat_active_no_temp_override(&this->tempomat)  ==>  epc_input_mode == accelerator;
    */
    void speed_controller_verify_epc_input_mode(speed_controller_t* this)
    {
    	speed_controller_run(this);
    }
    
    
    /*@ speed_controller_inv
    	behavior override: assumes (&this->tempomat)->active;
    		ensures tempomat_handler_driver_input_accelerate  ==>  epc_input_mode == accelerator;
    */
    void speed_controller_verify_override(speed_controller_t* this)
    {
    	speed_controller_run(this);
    }
    
    c file icon cc.c (12,157 bytes) 2011-10-27 17:10 +

-Relationships
+Relationships

-Notes

~0002432

cmarche (developer)

I see, the reason is that the "val" identifier is a keyword in Why3 and Jessie did not take this into account.

A quick work-around is to rename the variable 'val' in your code

Fixed in Why SVN Nitrogen branch

~0003782

signoles (manager)

Fixed in Frama-C Oxygen + Why 2.32.
+Notes

-Issue History
Date Modified Username Field Change
2011-10-27 17:10 boris New Issue
2011-10-27 17:10 boris Status new => assigned
2011-10-27 17:10 boris Assigned To => cmarche
2011-10-27 17:10 boris File Added: cc.c
2011-10-28 06:57 cmarche Note Added: 0002432
2011-10-28 06:58 cmarche Status assigned => resolved
2011-10-28 06:58 cmarche Resolution open => fixed
2013-03-27 09:43 signoles Note Added: 0003782
2013-03-27 09:44 signoles Fixed in Version => Frama-C Oxygen-20120901
2013-03-27 09:44 signoles Status resolved => closed
+Issue History