From 04ab514f310cd1ae4b92d6e5fae2ae8fb7e66845 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Wed, 28 Dec 2022 10:06:23 -0500 Subject: [PATCH] Renamed proof headers. Removed "verifast" prefix where unnecessary. --- .../proof/lock_predicates.h | 512 ++++++++++++++++++ ...fast_port_contracts.h => port_contracts.h} | 6 +- ...running_states.h => task_running_states.h} | 6 +- .../proof/verifast_lock_predicates.h | 8 +- .../proof_setup/{verifast_asm.h => asm.h} | 6 +- .../{verifast_proof_defs.h => proof_defs.h} | 4 +- .../proof_setup/sys/cdefs.h | 2 +- .../tasks/vTaskSwitchContext/src/tasks.c | 8 +- 8 files changed, 532 insertions(+), 20 deletions(-) create mode 100644 Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h rename Test/VeriFast/tasks/vTaskSwitchContext/proof/{verifast_port_contracts.h => port_contracts.h} (95%) rename Test/VeriFast/tasks/vTaskSwitchContext/proof/{verifast_task_running_states.h => task_running_states.h} (91%) rename Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/{verifast_asm.h => asm.h} (93%) rename Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/{verifast_proof_defs.h => proof_defs.h} (93%) diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h new file mode 100644 index 000000000..9a185ee7f --- /dev/null +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h @@ -0,0 +1,512 @@ +#ifndef LOCK_PREDICATES_H +#define LOCK_PREDICATES_H + +#include "task_running_states.h" + + +/* We follow a minimalistic approach during the definition of the + * lock predicates. So far, the only encapsulate the resources and + * invariants required to verify `vTaskSwitchContext`. + * We are going to extend and refine them when we proceed to verify + * other parts of FRTOS. + */ + +#include "verifast_lists_extended.h" + + + +/* ---------------------------------------------------------------------- + * Core local data and access restrictions. + * Some data in FreeRTOS such as the pointer to TCB of the task running + * on core `C` may only be accessed from core `C`. Such core-local data + * protected by deactivating interrupts. + */ + +/*@ +predicate interruptState_p(uint32_t coreID, uint32_t state); + +fixpoint bool interruptsDisabled_f(uint32_t); + +predicate coreLocalInterruptInv_p() = + [0.5]pointer(&pxCurrentTCBs[coreID_f], ?currentTCB) &*& + //pubTCB_p(currentTCB, 0) &*& + integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*& + coreLocalSeg_TCB_p(currentTCB, ?gCriticalNesting); +@*/ + + +/* ---------------------------------------------------------------------- + * Predicates relevant for all locks + */ + +/*@ +predicate locked_p(list< pair > lockHistory); +@*/ + + + +/* ---------------------------------------------------------------------- + * Task lock and associated global variables from `tasks.c` + */ + +/*@ +fixpoint int taskLockID_f(); + +// Represents an acquired task lock. +predicate taskLock_p(); + +// Represents the invariant associated with the the task lock, i.e., +// access permissions to the resources protected by the lock. +predicate taskLockInv_p(); +@*/ + +/* ---------------------------------------------------------------------- + * ISR lock and associated global variables from `tasks.c` + */ + +/*@ +fixpoint int isrLockID_f(); + +// Represents an unacquired ISR lock. +predicate isrLock_p(); + +// Represents the invariant associated with the the ISR lock, i.e., +// access permissions to the resources protected by the lock. +predicate isrLockInv_p(); +@*/ + + +/* ---------------------------------------------------------------------- + * Resources protected by both locks. + * Note that the task lock may never be acquired after the ISR lock. + */ + +/*@ +fixpoint int taskISRLockID_f(); + +predicate taskISRLockInv_p() = + _taskISRLockInv_p(_); + + +// Auxiliary predicate. Equal to the lock invariant above but exposes +// some details. +predicate _taskISRLockInv_p(UBaseType_t gTopReadyPriority) = + // Access to global variables + [0.5]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& + integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*& + integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _) + &*& + // top ready priority must be in range + integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, gTopReadyPriority) &*& + 0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES + &*& + // tasks / TCBs + exists_in_taskISRLockInv_p(?gTasks, ?gStates) + &*& + // (RP-All) Read permissions for every task + // and recording of task states in state list + // (∀t ∈ gTasks. + // [1/2]TCB_runState_p(t, _)) + // ∧ + // ∀i. ∀t. gTasks[i] == t -> gStates[i] == t->xTaskRunState + foreach(gTasks, readOnly_TCB_runState_p(gTasks, gStates)) + &*& + // (RP-Current) Read permission for task currently scheduled on this core + // (RP-All) + (RP-Current) => Write permission for scheduled task + [1/2]TCB_runState_p(gCurrentTCB, ?gCurrentTCB_state) &*& +// gCurrentTCB_state != taskTASK_NOT_RUNNING &*& + (gCurrentTCB_state == coreID_f() || gCurrentTCB_state == taskTASK_YIELDING) &*& + nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state + &*& + // (RP-Unsched) Read permissions for unscheduled tasks + // (RP-All) + (RP-Unsched) => Write permissions for unscheduled tasks + // ∀t ∈ tasks. t->xTaskState == taskTASK_NOT_RUNNING + // -> [1/2]shared_TCB_p(t, taskTASK_NOT_RUNNING) + foreach(gTasks, readOnly_TCB_runState_IF_not_running_p(gTasks, gStates)) + &*& + readyLists_p(?gCellLists, ?gOwnerLists) + &*& + // gTasks contains all relevant tasks + mem(gCurrentTCB, gTasks) == true + &*& + // ∀l ∈ gOwnerLists. l ⊆ gTasks + forall(gOwnerLists, (superset)(gTasks)) == true; + + +lemma void produce_taskISRLockInv(); +requires locked_p(?heldLocks) &*& + heldLocks == cons(?i, cons(?t, nil)) &*& + i == pair(?f_isr, isrLockID_f()) &*& + t == pair(?f_task, taskLockID_f()); +ensures locked_p( cons( pair(_, taskISRLockID_f()), heldLocks) ) &*& + taskISRLockInv_p(); + + +lemma void consume_taskISRLockInv(); +requires locked_p( cons( pair(_, taskISRLockID_f()), ?otherLocks) ) &*& + taskISRLockInv_p(); +ensures locked_p(otherLocks); + + + +// Auxiliary predicate to assing names to existentially quantified variables. +// Having multiple `exists` chunks on the heap makes matching against their +// arguments ambiguous in most cases. +predicate exists_in_taskISRLockInv_p(list gTasks, + list gStates) = + exists(gTasks) &*& + exists(gStates) &*& + length(gTasks) == length(gStates) &*& + distinct(gTasks) == true; + +// Auxiliary function that allows us to partially apply the list argument. +// +// Notes: +// - Partial application of fixpoint functions in VeriFast is not documented. +// The syntax for partially application is `()()` +// - VeriFast only supports partially applying the first argument, e.g., +// `(mem)(0)` is allowed but `(mem)(_)(nil)` is not. +fixpoint bool mem_list_elem(list xs, t x) { + return mem(x, xs); +} + +// Auxiliary predicate to allow foreach-quantification about fraction +// and reflection of `t->xTaskRunState` in state list. +predicate_ctor readOnly_TCB_runState_p + (list tasks, list states) + (TCB_t* t;) = + mem(t, tasks) == true &*& + [1/2]TCB_runState_p(t, nth(index_of(t, tasks), states)); + +predicate_ctor readOnly_TCB_runState_IF_not_running_p + (list tasks, list states) + (TCB_t* t;) = + mem(t, tasks) == true &*& + nth(index_of(t, tasks), states) == taskTASK_NOT_RUNNING + ? [1/2]TCB_runState_p(t, taskTASK_NOT_RUNNING) + : true; +@*/ + + + +/*@ +lemma void nonauto_nth_update(int i, int j, t y, list xs); + requires 0 <= i && i < length(xs) && 0 <= j && j < length(xs); + ensures nth(i, update(j, y, xs)) == (i == j ? y : nth(i, xs)); +@*/ + + + +// ----------------------------------------------------------------------- +// TODO: Move lemmas below to separate header file. + +/*@ +lemma void update_readOnly_TCB_runState(TCB_t* t, + list tasks, + list states, + int updatedIndex, + TaskRunning_t s) +requires readOnly_TCB_runState_p(tasks, states)(t) &*& + updatedIndex != index_of(t, tasks) &*& + mem(t, tasks) == true &*& + length(tasks) == length(states); +ensures readOnly_TCB_runState_p(tasks, update(updatedIndex, s, states))(t); +{ + list states2 = update(updatedIndex, s, states); + int t_index = index_of(t, tasks); + + if( updatedIndex < 0 || updatedIndex >= length(states) ) { + update_out_of_bounds(updatedIndex, s, states); + } else { + open readOnly_TCB_runState_p(tasks, states)(t); + open [1/2]TCB_runState_p(t, nth(t_index, states)); + + mem_index_of(t, tasks); + nth_update(t_index, updatedIndex, s, states); + assert( nth(t_index, states) == nth(t_index, states2) ); + + close [1/2]TCB_runState_p(t, nth(t_index, states2)); + close readOnly_TCB_runState_p(tasks, states2)(t); + } +} + + +lemma void update_foreach_readOnly_TCB_runState(TCB_t* updatedTask, + list tasks, + list subTasks, + list states, + list states2, + TaskRunning_t s) +requires + mem(updatedTask, tasks) == true &*& + length(tasks) == length(states) &*& + foreach(subTasks, readOnly_TCB_runState_p(tasks, states)) &*& + states2 == update(index_of(updatedTask, tasks), s, states) &*& + distinct(tasks) == true &*& + mem(updatedTask, subTasks) == false &*& + subset(subTasks, tasks) == true; +ensures + foreach(subTasks, readOnly_TCB_runState_p(tasks, states2)); +{ + switch(subTasks) { + case nil: + open foreach(nil, readOnly_TCB_runState_p(tasks, states)); + close foreach(nil, readOnly_TCB_runState_p(tasks, states2)); + case cons(h, rest): + int index = index_of(updatedTask, tasks); +// distinct_mem_remove(t, tasks); +// neq_mem_remove(h, t, tasks); +// index_of_different(h, t, tasks); + open foreach(subTasks, readOnly_TCB_runState_p(tasks, states)); + assert( updatedTask != h ); + index_of_different(updatedTask, h, tasks); + assert( index != index_of(h, tasks) ); + update_readOnly_TCB_runState(h, tasks, states, index, s); + assert( mem(updatedTask, rest) == false ); + update_foreach_readOnly_TCB_runState(updatedTask, tasks, rest, + states, states2, s); + close foreach(subTasks, readOnly_TCB_runState_p(tasks, states2)); + } +} + + +lemma void close_updated_foreach_readOnly_TCB_runState(TCB_t* updatedTask, + list tasks, + list states, + list states2, + TaskRunning_t s) +requires + mem(updatedTask, tasks) == true &*& + length(states) == length(tasks) &*& + distinct(tasks) == true &*& + foreach(remove(updatedTask, tasks), readOnly_TCB_runState_p(tasks, states)) &*& + states2 == update(index_of(updatedTask, tasks), s, states) &*& + [1/2]TCB_runState_p(updatedTask, s); +ensures + foreach(tasks, readOnly_TCB_runState_p(tasks, states2)); +{ + distinct_mem_remove(updatedTask, tasks); + remove_result_subset(updatedTask, tasks); + + close readOnly_TCB_runState_p(tasks, states2)(updatedTask); + update_foreach_readOnly_TCB_runState(updatedTask, tasks, + remove(updatedTask, tasks), + states, states2, s); + foreach_unremove(updatedTask, tasks); +} + + +lemma void stopUpdate_foreach_readOnly_TCB_runState_IF_not_running + (TCB_t* stoppedTask, list tasks, list subTasks, + list states, list states2) +requires + distinct(tasks) == true &*& + distinct(subTasks) == true &*& + length(tasks) == length(states) &*& + foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, states)) &*& + states2 == update(index_of(stoppedTask, tasks), taskTASK_NOT_RUNNING, states) &*& + nth(index_of(stoppedTask, tasks), states) != taskTASK_NOT_RUNNING &*& + subset(subTasks, tasks) == true &*& + mem(stoppedTask, tasks) == true &*& + mem(stoppedTask, subTasks) + ? [1/2]TCB_runState_p(stoppedTask, taskTASK_NOT_RUNNING) + : true; +ensures + foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, states2)); +{ + switch(subTasks) { + case nil: + open foreach(nil, readOnly_TCB_runState_IF_not_running_p(tasks, states)); + close foreach(nil, readOnly_TCB_runState_IF_not_running_p(tasks, states2)); + case cons(h, t): + if( h == stoppedTask ) { + assert( remove(stoppedTask, subTasks) == t ); + distinct_mem_remove(stoppedTask, subTasks); + assert( mem(stoppedTask, t) == false ); + mem_index_of(stoppedTask, tasks); + } else { + mem_index_of(stoppedTask, tasks); + nth_update(index_of(h, tasks), index_of(stoppedTask, tasks), taskTASK_NOT_RUNNING, states); + index_of_different(h, stoppedTask, tasks); + assert( index_of(h, tasks) != index_of(stoppedTask, tasks) ); + assert( nth(index_of(h, tasks), states) == nth(index_of(h, tasks), states2) ); + } + + nth_update(index_of(stoppedTask, tasks), index_of(stoppedTask, tasks), taskTASK_NOT_RUNNING, states); + open foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, states)); + open readOnly_TCB_runState_IF_not_running_p(tasks, states)(h); + assert( nth(index_of(stoppedTask, tasks), states2) == taskTASK_NOT_RUNNING ); + close readOnly_TCB_runState_IF_not_running_p(tasks, states2)(h); + stopUpdate_foreach_readOnly_TCB_runState_IF_not_running + (stoppedTask, tasks, t, states, states2); + close foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, states2)); + } +} + +lemma void updateUnaffectedStates_in_foreach_readOnly_TCB_runState_IF_not_running + (TCB_t* updatedTask, list tasks, list subTasks, + list states, list updatedStates, + TaskRunning_t s) +requires + distinct(tasks) == true &*& + distinct(subTasks) == true &*& + length(tasks) == length(states) &*& + mem(updatedTask, tasks) == true &*& + mem(updatedTask, subTasks) == false &*& + subset(subTasks, tasks) == true &*& + foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, states)) &*& + updatedStates == update(index_of(updatedTask, tasks), s, states); +ensures + foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)); +{ + switch(subTasks) { + case nil: + open foreach(nil, readOnly_TCB_runState_IF_not_running_p(tasks, states)); + close foreach(nil, readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)); + case cons(h, t): + open foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, states)); + + // Prove that update preserves state of `h`. + index_of_different(h, updatedTask, tasks); + nth_update(index_of(h, tasks), index_of(updatedTask, tasks), s, states); + assert( nth(index_of(h, tasks), states) == nth(index_of(h, tasks), updatedStates) ); + + open readOnly_TCB_runState_IF_not_running_p(tasks, states)(h); + close readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)(h); + updateUnaffectedStates_in_foreach_readOnly_TCB_runState_IF_not_running + (updatedTask, tasks, t, states, updatedStates, s); + close foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)); + } +} + +lemma void startUpdate_foreach_readOnly_TCB_runState_IF_not_running + (TCB_t* startedTask, list tasks, + list states, list updatedStates, + int coreID) +requires + distinct(tasks) == true &*& + length(tasks) == length(states) &*& + mem(startedTask, tasks) == true &*& + foreach(remove(startedTask, tasks), readOnly_TCB_runState_IF_not_running_p(tasks, states)) &*& + updatedStates == update(index_of(startedTask, tasks), coreID, states) &*& + 0 <= coreID &*& coreID < configNUM_CORES; +ensures + foreach(tasks, readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)); +{ + distinct_remove(startedTask, tasks); + distinct_mem_remove(startedTask, tasks); + remove_result_subset(startedTask, tasks); + updateUnaffectedStates_in_foreach_readOnly_TCB_runState_IF_not_running + (startedTask, tasks, remove(startedTask, tasks), states, updatedStates, + coreID); + + assert( foreach(remove(startedTask, tasks), readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)) ); + close readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)(startedTask); + foreach_unremove(startedTask, tasks); +} + +lemma void scheduleRunning_in_foreach_readOnly_TCB_runState_IF_not_running + (TCB_t* runningTask, list tasks, + list states, list updatedStates, + int coreID) +requires + distinct(tasks) == true &*& + length(tasks) == length(states) &*& + mem(runningTask, tasks) == true &*& + (nth(index_of(runningTask, tasks), states) == coreID + || nth(index_of(runningTask, tasks), states) == taskTASK_YIELDING) + &*& + foreach(tasks, readOnly_TCB_runState_IF_not_running_p(tasks, states)) &*& + updatedStates == update(index_of(runningTask, tasks), coreID, states) &*& + 0 <= coreID &*& coreID < configNUM_CORES; +ensures + foreach(tasks, readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)) &*& + nth(index_of(runningTask, tasks), updatedStates) == coreID; +{ + switch(tasks) { + case nil: + open foreach(nil, readOnly_TCB_runState_IF_not_running_p(tasks, states)); + close foreach(nil, readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)); + case cons(h, t): + foreach_remove(runningTask, tasks); + + distinct_remove(runningTask, tasks); + distinct_mem_remove(runningTask, tasks); + remove_result_subset(runningTask, tasks); + updateUnaffectedStates_in_foreach_readOnly_TCB_runState_IF_not_running + (runningTask, tasks, remove(runningTask, tasks), + states, updatedStates, coreID); + + open readOnly_TCB_runState_IF_not_running_p(tasks, states)(runningTask); + close readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)(runningTask); + + foreach_unremove(runningTask, tasks); + } +} +@*/ + + +/*@ +lemma list def_state1(list tasks, + list states, + TCB_t* currentTask, + TCB_t* readyTask) +requires + distinct(tasks) == true &*& + length(tasks) == length(states) &*& + currentTask != readyTask &*& + mem(currentTask, tasks) == true &*& + mem(readyTask, tasks) == true &*& + nth(index_of(readyTask, tasks), states) == taskTASK_NOT_RUNNING; +ensures + result == update(index_of(currentTask, tasks), taskTASK_NOT_RUNNING, states) &*& + nth(index_of(readyTask, tasks), result) == taskTASK_NOT_RUNNING &*& + nth(index_of(currentTask, tasks), result) == taskTASK_NOT_RUNNING; +{ + list states1 = + update(index_of(currentTask, tasks), taskTASK_NOT_RUNNING, states); + + mem_index_of(currentTask, tasks); + mem_index_of(readyTask, tasks); + nth_update(index_of(readyTask, tasks), index_of(currentTask, tasks), taskTASK_NOT_RUNNING, states); + + return states1; +} + +lemma list def_state2(list tasks, + list states, + TCB_t* currentTask, + TCB_t* readyTask, + int coreID) +requires + distinct(tasks) == true &*& + length(tasks) == length(states) &*& + currentTask != readyTask &*& + mem(currentTask, tasks) == true &*& + mem(readyTask, tasks) == true &*& + nth(index_of(readyTask, tasks), states) == taskTASK_NOT_RUNNING &*& + nth(index_of(currentTask, tasks), states) != taskTASK_NOT_RUNNING &*& + 0 <= coreID &*& coreID < configNUM_CORES; +ensures + result == + update(index_of(readyTask, tasks), coreID, + update(index_of(currentTask, tasks), taskTASK_NOT_RUNNING, states)) + &*& + nth(index_of(readyTask, tasks), result) == coreID &*& + nth(index_of(currentTask, tasks), result) == taskTASK_NOT_RUNNING; +{ + list states1 = def_state1(tasks, states, currentTask, readyTask); + + list states2 = + update(index_of(readyTask, tasks), coreID, states1); + + return states2; +} +@*/ + + + + + + +#endif /* LOCK_PREDICATES_H */ \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_port_contracts.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/port_contracts.h similarity index 95% rename from Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_port_contracts.h rename to Test/VeriFast/tasks/vTaskSwitchContext/proof/port_contracts.h index 620e82b75..eedbca87f 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_port_contracts.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/port_contracts.h @@ -1,5 +1,5 @@ -#ifndef VERIFAST_PORT_CONTRACTS_H -#define VERIFAST_PORT_CONTRACTS_H +#ifndef PORT_CONTRACTS_H +#define PORT_CONTRACTS_H // We want our proofs to hold for an arbitrary number of cores. @@ -76,4 +76,4 @@ void VF__portRELEASE_ISR_LOCK(); //@ ensures [f]isrLock_p() &*& locked_p(heldLocks); -#endif /* VERIFAST_PORT_CONTRACTS_H */ \ No newline at end of file +#endif /* PORT_CONTRACTS_H */ \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_task_running_states.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/task_running_states.h similarity index 91% rename from Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_task_running_states.h rename to Test/VeriFast/tasks/vTaskSwitchContext/proof/task_running_states.h index dcfaa9d69..80d8c7a57 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_task_running_states.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/task_running_states.h @@ -1,5 +1,5 @@ -#ifndef VERIFAST_TASK_RUNNING_STATES_H -#define VERIFAST_TASK_RUNNING_STATES_H +#ifndef TASK_RUNNING_STATES_H +#define TASK_RUNNING_STATES_H /* The source file `tasks.c` defines macros to denote the running states of * tasks: @@ -43,4 +43,4 @@ void validate_taskTASK_YIELDING_value() //@ assert( gVal == val ); } -#endif /* VERIFAST_TASK_RUNNING_STATES_H */ \ No newline at end of file +#endif /* TASK_RUNNING_STATES_H */ \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h index 3c9b50f08..9a185ee7f 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h @@ -1,7 +1,7 @@ -#ifndef VERIFAST_LOCK_PREDICATES_H -#define VERIFAST_LOCK_PREDICATES_H +#ifndef LOCK_PREDICATES_H +#define LOCK_PREDICATES_H -#include "verifast_task_running_states.h" +#include "task_running_states.h" /* We follow a minimalistic approach during the definition of the @@ -509,4 +509,4 @@ ensures -#endif /* VERIFAST_LOCK_PREDICATES_H */ \ No newline at end of file +#endif /* LOCK_PREDICATES_H */ \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_asm.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/asm.h similarity index 93% rename from Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_asm.h rename to Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/asm.h index faf769067..83da579c1 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_asm.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/asm.h @@ -1,5 +1,5 @@ -#ifndef VERIFAST_ASM_H -#define VERIFAST_ASM_H +#ifndef ASM_H +#define ASM_H /* VeriFast does not support inline assembler. * The following definitions replace macros that would normally evaluate to @@ -32,4 +32,4 @@ bool assert_fct(bool b, const char*) //#undef portDISABLE_INTERRUPTS //#define portDISABLE_INTERRUPTS() assert_fct(false, "portDISABLE_INTERRUPTS") -#endif /* VERIFAST_ASM_H */ \ No newline at end of file +#endif /* ASM_H */ \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_proof_defs.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/proof_defs.h similarity index 93% rename from Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_proof_defs.h rename to Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/proof_defs.h index b1e288e2c..25fefd3bb 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_proof_defs.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/proof_defs.h @@ -4,7 +4,7 @@ */ -#ifndef VERIFAST_DEFS_H +#ifndef PROOF_DEFS_H // Delete keywords VeriFast canot parse (in some contexts) #define inline #define __always_inline @@ -24,4 +24,4 @@ #undef assert #undef configASSERT #define configASSERT(x) assert(x) -#endif /* VERIFAST_DEFS_H */ +#endif /* PROOF_DEFS_H */ diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/sys/cdefs.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/sys/cdefs.h index 0940dd633..9a05dfb24 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/sys/cdefs.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/sys/cdefs.h @@ -76,7 +76,7 @@ * e.g., `tasks.c`. But it seems like the contained defines are not propagated * to this file. */ - #include "verifast_proof_defs.h" + #include "proof_defs.h" #endif #if defined(__cplusplus) diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c index c92cc7cfc..917960863 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c +++ b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c @@ -74,14 +74,14 @@ * original ones have been included. */ #ifdef VERIFAST - #include "verifast_proof_defs.h" + #include "proof_defs.h" #include "stack_predicates.h" #include "task_predicates.h" #include "ready_list_predicates.h" #include "verifast_RP2040_axioms.h" - #include "verifast_asm.h" - #include "verifast_port_contracts.h" - #include "verifast_lock_predicates.h" + #include "asm.h" + #include "port_contracts.h" + #include "lock_predicates.h" #include "verifast_lists_extended.h" #include "single_core_proofs/scp_list_predicates.h" #include "single_core_proofs_extended/scp_list_predicates_extended.h"