Skip to content

Commit 1b8c2cd

Browse files
wadoonmattulbrich
wadoon
authored and
mattulbrich
committed
fix proof scripts in inf-flow
1 parent bfdc4c4 commit 1b8c2cd

File tree

139 files changed

+139
-139
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

139 files changed

+139
-139
lines changed

‎key.core.rifl/src/main/resources/de.uka.ilkd.key.util/rifl/blueprint_rifl.key‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747
"class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO",
4848
}
4949

50-
\proofScript "macro 'infflow-autopilot';"
50+
\proofScript { macro "infflow-autopilot"; }
5151

5252
\proof {
5353
(autoModeTime "0")

‎key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_no_return_secure(int)).Non-interference contract.0.m.key‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747
"class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO",
4848
}
4949

50-
\proofScript "macro 'infflow-autopilot';"
50+
\proofScript { macro "infflow-autopilot"; }
5151

5252
\proof {
5353
(keyLog "0" (keyUser "kirsten" ) (keyVersion "de4c58c270d097d36f2ff647cca5aa0c0c488891"))

‎key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__block_while_secure(int)).Non-interference contract.0.m.key‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747
"class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO",
4848
}
4949

50-
\proofScript "macro 'infflow-autopilot';"
50+
\proofScript { macro "infflow-autopilot"; }
5151

5252
\proof {
5353
(keyLog "0" (keyUser "kirsten" ) (keyVersion "de4c58c270d097d36f2ff647cca5aa0c0c488891"))

‎key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_1(int)).Non-interference contract.0.m.key‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747
"class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO",
4848
}
4949

50-
\proofScript "macro 'infflow-autopilot';"
50+
\proofScript { macro "infflow-autopilot"; }
5151

5252
\proof {
5353
(keyLog "0" (keyUser "kirsten" ) (keyVersion "de4c58c270d097d36f2ff647cca5aa0c0c488891"))

‎key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_3(int)).Non-interference contract.0.m.key‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747
"class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO",
4848
}
4949

50-
\proofScript "macro 'infflow-autopilot';"
50+
\proofScript { macro "infflow-autopilot"; }
5151

5252
\proof {
5353
(keyLog "0" (keyUser "kirsten" ) (keyVersion "de4c58c270d097d36f2ff647cca5aa0c0c488891"))

‎key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__insecure_4(int)).Non-interference contract.0.m.key‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747
"class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO",
4848
}
4949

50-
\proofScript "macro 'infflow-autopilot';"
50+
\proofScript { macro "infflow-autopilot"; }
5151

5252
\proof {
5353
(keyLog "0" (keyUser "kirsten" ) (keyVersion "de4c58c270d097d36f2ff647cca5aa0c0c488891"))

‎key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_1(int)).Non-interference contract.0.m.key‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747
"class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO",
4848
}
4949

50-
\proofScript "macro 'infflow-autopilot';"
50+
\proofScript { macro "infflow-autopilot"; }
5151

5252
\proof {
5353
(keyLog "0" (keyUser "kirsten" ) (keyVersion "de4c58c270d097d36f2ff647cca5aa0c0c488891"))

‎key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_2(int)).Non-interference contract.0.m.key‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747
"class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO",
4848
}
4949

50-
\proofScript "macro 'infflow-autopilot';"
50+
\proofScript { macro "infflow-autopilot"; }
5151

5252
\proof {
5353
(keyLog "0" (keyUser "kirsten" ) (keyVersion "de4c58c270d097d36f2ff647cca5aa0c0c488891"))

‎key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_3(int)).Non-interference contract.0.m.key‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747
"class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO",
4848
}
4949

50-
\proofScript "macro 'infflow-autopilot';"
50+
\proofScript { macro "infflow-autopilot"; }
5151

5252
\proof {
5353
(keyLog "0" (keyUser "kirsten" ) (keyVersion "de4c58c270d097d36f2ff647cca5aa0c0c488891"))

‎key.ui/examples/InformationFlow/BlockContracts/contract.IFBlockExamples(contract.IFBlockExamples__secure_4(int)).Non-interference contract.0.m.key‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747
"class": "de.uka.ilkd.key.informationflow.po.InfFlowContractPO",
4848
}
4949

50-
\proofScript "macro 'infflow-autopilot';"
50+
\proofScript { macro "infflow-autopilot"; }
5151

5252
\proof {
5353
(keyLog "0" (keyUser "kirsten" ) (keyVersion "de4c58c270d097d36f2ff647cca5aa0c0c488891"))

0 commit comments

Comments
 (0)