TrigDeveloper1 TrigDevelopment

TrigDevelopment / pre-result.c

Created March 22, 2021 11:57

	struct container {
	int counter;
	};

	/*@ requires \valid(some_container);
	requires some_container->counter == 0;
	ensures \result->counter == \at(\result->counter, Pre) + 1;
	*/
	struct container * f(struct container * some_container) {
	some_container->counter = 1;

TrigDevelopment / arithmetic-with-check.c

Created March 22, 2021 10:40

	#define INT_MAX 2147483647

	typedef struct {
	int counter;
	} atomic_t;

	/*@ requires v.counter < INT_MAX;
	ensures v.counter == \old(v.counter) + 1;
	*/
	static inline void atomic_inc(atomic_t v);

TrigDevelopment / arithmetic-without-check.c

Created March 22, 2021 10:36

	typedef struct {
	int counter;
	} atomic_t;

	/*@ ensures v.counter == \old(v.counter) + 1;
	*/
	static inline void atomic_inc(atomic_t v);

	/*@ assigns \nothing;
	ensures 1 == 0;

TrigDevelopment / behaviours-assigns.c

Created March 22, 2021 07:57

TrigDevelopment / predicate-in-assigns.c

Last active March 22, 2021 07:54

TrigDevelopment / conditional-assigns.c

Created March 22, 2021 07:30

	int a;
	int b;
	void child(int child_argument);

	/*@ requires parent_argument == 0;
	assigns a;
	*/
	void parent(int parent_argument)
	{
	child(parent_argument);