len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-12 06:35:19 -05:00
Code Issues Projects Releases Packages Wiki Activity

Commented old opening and closing lemmas out and switched back from Z3 to VF standard SMT solver

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-28 12:20:30 -05:00
parent c0df2a2894
commit 2048fb85da
2 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h
View file

@ -8,7 +8,7 @@
* allows accesses to `pxItem->pxNext`. * allows accesses to `pxItem->pxNext`.
*/ */
/*@ /* @
lemma void DLS_end_next_open(struct xLIST* pxList, struct xLIST_ITEM* pxItem) lemma void DLS_end_next_open(struct xLIST* pxList, struct xLIST_ITEM* pxItem)
requires requires
DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, pxList) &*& DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, pxList) &*&
@ -363,14 +363,14 @@ ensures
* apply to the use cases they are meant for. * apply to the use cases they are meant for.
*/ */
void lemma_validation__DLS_item_next(struct xLIST_ITEM* pxTaskItem) void lemma_validation__DLS_item_next(struct xLIST_ITEM* pxTaskItem)
/*@ requires /* @ requires
DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*& DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*&
mem(pxTaskItem, gCells) == true &*& mem(pxTaskItem, gCells) == true &*&
gEnd == head(gCells) &*& gEnd == head(gCells) &*&
length(gCells) == length(gVals) &*& length(gCells) == length(gVals) &*&
length(gCells) > 1; length(gCells) > 1;
@*/ @*/
/*@ ensures /* @ ensures
DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*& DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*&
mem(pxTaskItem, gCells) == true; mem(pxTaskItem, gCells) == true;
@*/ @*/

3
verification/verifast/start-vfide--preprocessed.sh
View file

@ -13,6 +13,7 @@ PP_SCRIPT_DIR="$START_WD/custom_build_scripts_RP2040"
PP_SCRIPT="./preprocess_tasks_c.sh" PP_SCRIPT="./preprocess_tasks_c.sh"
PP_TASK_C="$START_WD/preprocessed_files/tasks__pp.c" PP_TASK_C="$START_WD/preprocessed_files/tasks__pp.c"
#FONT_SIZE=20
FONT_SIZE=17 FONT_SIZE=17
# Flags to SKIP expensive proofs: # Flags to SKIP expensive proofs:
@ -38,6 +39,6 @@ echo "\n\nPreprocessing script finished\n\n"
-I proofs \ -I proofs \
-codeFont "$FONT_SIZE" -traceFont "$FONT_SIZE" \ -codeFont "$FONT_SIZE" -traceFont "$FONT_SIZE" \
-assume_no_provenance \ -assume_no_provenance \
-prover z3v4.5 # -prover z3v4.5
# -target 32bit -prover z3v4.5 \ # -target 32bit -prover z3v4.5 \
# TODO: If we set the target to 32bit, VF create `uint` chunks instead of `char` chunks during malloc # TODO: If we set the target to 32bit, VF create `uint` chunks instead of `char` chunks during malloc