Commits (1)
......@@ -25,7 +25,6 @@
ensures ((struct capture_framaC *) \result)->gen.init == true;
ensures ((struct capture_framaC *) \result)->index == index;
ensures \old(((struct capture_framaC *) _devs[index])->gen.init) == false ==> ((struct capture_framaC *) \result)->value == 0;
assigns *((struct capture_framaC *) _devs[index]);
complete behaviors;
disjoint behaviors;
*/
......
......@@ -30,4 +30,19 @@ void framaC_capture_setValue(struct capture *capture, uint32_t value);
HAL_DEFINE_GLOBAL_ARRAY(capture);
#define FRAMAC_CAPTURE_ID(_id) HAL_GET_ID(capture, framaC, framaC_capture_##_id)
/*@
requires \valid((struct capture_generic *) t);
behavior isInit:
assumes ((struct capture_generic *) t)->init == true;
ensures \result == CAPTURE_ALREDY_INITED;
assigns \nothing;
behavior isNotInit:
assumes ((struct capture_generic *) t)->init == false;
ensures ((struct capture_generic *) t)->init == true;
ensures \result == 0;
assigns ((struct capture_generic *) t)->init;
disjoint behaviors;
*/
int32_t capture_generic_init(struct capture *t);
#endif
/* SPDX-License-Identifier: MIT */
/*
* Author: Andreas Werner <kernel@andy89.org>
* Date: 2021
*/
#ifndef FRAMA_C_GPIO_H_
#define FRAMA_C_GPIO_H_
#include <gpio.h>
#define GPIO_PRV
#include <gpio_prv.h>
/*@
requires \valid((struct gpio_generic *) g);
behavior isInit:
assumes ((struct gpio_generic *) g)->init == true;
ensures \result == GPIO_ALREDY_INITED;
assigns \nothing;
behavior isNotInit:
assumes ((struct gpio_generic *) g)->init == false;
ensures ((struct gpio_generic *) g)->init == true;
ensures \result == 0;
assigns ((struct gpio_generic *) g)->init;
disjoint behaviors;
*/
int32_t gpio_genericInit(struct gpio *g);
#endif
......@@ -29,4 +29,19 @@ HAL_DEFINE_GLOBAL_ARRAY(pwm);
uint64_t framaC_pwm_getPeriod(struct pwm *pwm);
uint64_t framaC_pwm_getDutyCycle(struct pwm *pwm);
/*@
requires \valid((struct pwm_generic *) p);
behavior isInit:
assumes ((struct pwm_generic *) p)->init == true;
ensures \result == PWM_ALREDY_INITED;
assigns \nothing;
behavior isNotInit:
assumes ((struct pwm_generic *) p)->init == false;
ensures ((struct pwm_generic *) p)->init == true;
ensures \result == 0;
assigns ((struct pwm_generic *) p)->init;
disjoint behaviors;
*/
int32_t pwm_generic_init(struct pwm *p);
#endif
......@@ -32,4 +32,18 @@ void framaC_timer_overflow(struct timer *t);
HAL_DEFINE_GLOBAL_ARRAY(timer);
#define FRAMAC_TIMER_ID(_id) HAL_GET_ID(timer, framaC, framaC_timer_##_id)
/*@
requires \valid((struct timer_generic *) t);
behavior isInit:
assumes ((struct timer_generic *) t)->init == true;
ensures \result == TIMER_ALREDY_INITED;
assigns \nothing;
behavior isNotInit:
assumes ((struct timer_generic *) t)->init == false;
ensures ((struct timer_generic *) t)->init == true;
ensures \result == 0;
assigns ((struct timer_generic *) t)->init;
disjoint behaviors;
*/
int32_t timer_generic_init(struct timer *t);
#endif