Skip to content
This repository has been archived by the owner on Nov 5, 2021. It is now read-only.

Commit

Permalink
Added Evaluation data
Browse files Browse the repository at this point in the history
  • Loading branch information
@TheMC47
TheMC47 committed Sep 8, 2021
1 parent ce2ab70 commit 5aed1a3
Show file tree
Hide file tree
Showing 210 changed files with 210 additions and 0 deletions.
1 change: 1 addition & 0 deletions evaluation/BDD_0.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"reports":[{"theory":"BDD.BinDag","report":{"results":[{"name":"global_attribute_on_unnamed_lemma","stopPosition":"37:12","stopOffset":1121,"edit":null,"startOffset":1117,"severity":"High","startPosition":"37:8","commands":[-375]},{"name":"global_attribute_on_unnamed_lemma","stopPosition":"40:12","stopOffset":1185,"edit":null,"startOffset":1181,"severity":"High","startPosition":"40:8","commands":[-379]},{"name":"global_attribute_on_unnamed_lemma","stopPosition":"43:12","stopOffset":1249,"edit":null,"startOffset":1245,"severity":"High","startPosition":"43:8","commands":[-383]},{"name":"global_attribute_on_unnamed_lemma","stopPosition":"46:12","stopOffset":1313,"edit":null,"startOffset":1309,"severity":"High","startPosition":"46:8","commands":[-387]}]},"timing":376},{"theory":"BDD.General","report":{"results":[{"name":"use_by","stopPosition":"140:5","stopOffset":5473,"edit":{"startOffset":5353,"stopOffset":5473,"replacement":"by (induct t rule: bdt_fn.induct) (auto split: option.splits)","msg":null},"startOffset":5353,"severity":"Low","startPosition":"138:1","commands":[-15714,-15716,-15718]},{"name":"use_by","stopPosition":"146:5","stopOffset":5664,"edit":{"startOffset":5589,"stopOffset":5664,"replacement":"by (induct t rule: bdt_fn.induct) (auto split: option.splits)","msg":null},"startOffset":5589,"severity":"Low","startPosition":"144:1","commands":[-15722,-15724,-15726]},{"name":"lemma_transforming_attribute","stopPosition":"247:36","stopOffset":8808,"edit":null,"startOffset":8797,"severity":"Medium","startPosition":"247:25","commands":[-15896]},{"name":"unrestricted_auto","stopPosition":"288:11","stopOffset":9849,"edit":null,"startOffset":9839,"severity":"High","startPosition":"288:1","commands":[-15966]},{"name":"use_by","stopPosition":"298:5","stopOffset":10125,"edit":{"startOffset":10092,"stopOffset":10125,"replacement":"by (simp add: dag_setofD)","msg":null},"startOffset":10092,"severity":"Low","startPosition":"297:1","commands":[-15982,-15984]},{"name":"use_by","stopPosition":"302:5","stopOffset":10308,"edit":{"startOffset":10275,"stopOffset":10308,"replacement":"by (simp add: dag_setofD)","msg":null},"startOffset":10275,"severity":"Low","startPosition":"301:1","commands":[-15988,-15990]},{"name":"implicit_rule","stopPosition":"655:13","stopOffset":21350,"edit":null,"startOffset":21346,"severity":"Medium","startPosition":"655:9","commands":[-16738]},{"name":"implicit_rule","stopPosition":"656:13","stopOffset":21363,"edit":null,"startOffset":21359,"severity":"Medium","startPosition":"656:9","commands":[-16740]},{"name":"implicit_rule","stopPosition":"661:13","stopOffset":21450,"edit":null,"startOffset":21446,"severity":"Medium","startPosition":"661:9","commands":[-16750]},{"name":"use_by","stopPosition":"757:5","stopOffset":25705,"edit":{"startOffset":25673,"stopOffset":25705,"replacement":"by (simp add: wf_ll_def)","msg":null},"startOffset":25673,"severity":"Low","startPosition":"756:1","commands":[-16832,-16834]},{"name":"use_by","stopPosition":"899:5","stopOffset":29431,"edit":{"startOffset":29416,"stopOffset":29431,"replacement":"by auto","msg":null},"startOffset":29416,"severity":"Low","startPosition":"898:1","commands":[-17178,-17180]},{"name":"use_by","stopPosition":"1383:7","stopOffset":45304,"edit":{"startOffset":45240,"stopOffset":45304,"replacement":"by (simp add: Nodes_def) (simp add: set_split)","msg":null},"startOffset":45240,"severity":"Low","startPosition":"1381:3","commands":[-18340,-18342,-18344]},{"name":"implicit_rule","stopPosition":"1570:15","stopOffset":51945,"edit":null,"startOffset":51941,"severity":"Medium","startPosition":"1570:11","commands":[-18678]},{"name":"implicit_rule","stopPosition":"1625:19","stopOffset":54504,"edit":null,"startOffset":54500,"severity":"Medium","startPosition":"1625:15","commands":[-18786]},{"name":"implicit_rule","stopPosition":"1637:20","stopOffset":54922,"edit":null,"startOffset":54918,"severity":"Medium","startPosition":"1637:16","commands":[-18810]},{"name":"implicit_rule","stopPosition":"1685:23","stopOffset":57042,"edit":null,"startOffset":57038,"severity":"Medium","startPosition":"1685:19","commands":[-18934]},{"name":"use_by","stopPosition":"1822:5","stopOffset":60160,"edit":{"startOffset":60087,"stopOffset":60160,"replacement":"by (induct xs) (auto simp add: take_Cons split: nat.splits)","msg":null},"startOffset":60087,"severity":"Low","startPosition":"1820:1","commands":[-19192,-19194,-19196]},{"name":"use_by","stopPosition":"1885:7","stopOffset":62212,"edit":{"startOffset":62175,"stopOffset":62212,"replacement":"by (induct xs) auto","msg":null},"startOffset":62175,"severity":"Low","startPosition":"1883:3","commands":[-19282,-19284,-19286]}]},"timing":415},{"theory":"BDD.ProcedureSpecs","report":{"results":[]},"timing":1},{"theory":"BDD.EvalProof","report":{"results":[{"name":"use_by","stopPosition":"38:7","stopOffset":1361,"edit":{"startOffset":1286,"stopOffset":1361,"replacement":"by (hoare_rule HoarePartial.ProcRec1) (vcg spec=modifies)","msg":null},"startOffset":1286,"severity":"Low","startPosition":"36:3","commands":[-19315,-19317,-19319]}]},"timing":2},{"theory":"BDD.LevellistProof","report":{"results":[{"name":"use_by","stopPosition":"39:7","stopOffset":1502,"edit":{"startOffset":1427,"stopOffset":1502,"replacement":"by (hoare_rule HoarePartial.ProcRec1) (vcg spec=modifies)","msg":null},"startOffset":1427,"severity":"Low","startPosition":"37:3","commands":[-1036,-1038,-1040]},{"name":"use_by","stopPosition":"266:5","stopOffset":10078,"edit":{"startOffset":10062,"stopOffset":10078,"replacement":"by blast","msg":null},"startOffset":10062,"severity":"Low","startPosition":"265:1","commands":[-1262,-1264]},{"name":"apply_isar_switch","stopPosition":"311:8","stopOffset":12145,"edit":null,"startOffset":12138,"severity":"Medium","startPosition":"311:1","commands":[-1312]},{"name":"apply_isar_switch","stopPosition":"425:18","stopOffset":17553,"edit":null,"startOffset":17546,"severity":"Medium","startPosition":"425:11","commands":[-1474]},{"name":"apply_isar_switch","stopPosition":"633:16","stopOffset":26550,"edit":null,"startOffset":26543,"severity":"Medium","startPosition":"633:9","commands":[-1882]},{"name":"apply_isar_switch","stopPosition":"918:26","stopOffset":39175,"edit":null,"startOffset":39168,"severity":"Medium","startPosition":"918:19","commands":[-2472]},{"name":"apply_isar_switch","stopPosition":"1010:26","stopOffset":43781,"edit":null,"startOffset":43774,"severity":"Medium","startPosition":"1010:19","commands":[-2674]},{"name":"apply_isar_switch","stopPosition":"1122:26","stopOffset":49267,"edit":null,"startOffset":49260,"severity":"Medium","startPosition":"1122:19","commands":[-2906]},{"name":"apply_isar_switch","stopPosition":"1152:26","stopOffset":50778,"edit":null,"startOffset":50771,"severity":"Medium","startPosition":"1152:19","commands":[-2970]},{"name":"apply_isar_switch","stopPosition":"1172:26","stopOffset":51756,"edit":null,"startOffset":51749,"severity":"Medium","startPosition":"1172:19","commands":[-3022]}]},"timing":51},{"theory":"BDD.RepointProof","report":{"results":[{"name":"use_by","stopPosition":"40:7","stopOffset":1436,"edit":{"startOffset":1361,"stopOffset":1436,"replacement":"by (hoare_rule HoarePartial.ProcRec1) (vcg spec=modifies)","msg":null},"startOffset":1361,"severity":"Low","startPosition":"38:3","commands":[-14133,-14135,-14137]},{"name":"apply_isar_switch","stopPosition":"212:8","stopOffset":7824,"edit":null,"startOffset":7817,"severity":"Medium","startPosition":"212:1","commands":[-14449]},{"name":"apply_isar_switch","stopPosition":"423:8","stopOffset":17299,"edit":null,"startOffset":17292,"severity":"Medium","startPosition":"423:1","commands":[-14857]},{"name":"apply_isar_switch","stopPosition":"658:8","stopOffset":28336,"edit":null,"startOffset":28329,"severity":"Medium","startPosition":"658:1","commands":[-15265]}]},"timing":19},{"theory":"BDD.ShareRepProof","report":{"results":[{"name":"use_by","stopPosition":"38:7","stopOffset":1399,"edit":{"startOffset":1324,"stopOffset":1399,"replacement":"by (hoare_rule HoarePartial.ProcRec1) (vcg spec=modifies)","msg":null},"startOffset":1324,"severity":"Low","startPosition":"36:3","commands":[-8,-10,-12]}]},"timing":5},{"theory":"BDD.ShareReduceRepListProof","report":{"results":[{"name":"use_by","stopPosition":"38:7","stopOffset":1421,"edit":{"startOffset":1346,"stopOffset":1421,"replacement":"by (hoare_rule HoarePartial.ProcRec1) (vcg spec=modifies)","msg":null},"startOffset":1346,"severity":"Low","startPosition":"36:3","commands":[-3417,-3419,-3421]},{"name":"implicit_rule","stopPosition":"443:23","stopOffset":23099,"edit":null,"startOffset":23095,"severity":"Medium","startPosition":"443:19","commands":[-3927]},{"name":"implicit_rule","stopPosition":"452:23","stopOffset":23456,"edit":null,"startOffset":23452,"severity":"Medium","startPosition":"452:19","commands":[-3943]},{"name":"implicit_rule","stopPosition":"604:26","stopOffset":30964,"edit":null,"startOffset":30960,"severity":"Medium","startPosition":"604:22","commands":[-4201]},{"name":"implicit_rule","stopPosition":"685:26","stopOffset":35249,"edit":null,"startOffset":35245,"severity":"Medium","startPosition":"685:22","commands":[-4331]}]},"timing":66},{"theory":"BDD.NormalizeTotalProof","report":{"results":[{"name":"use_by","stopPosition":"41:7","stopOffset":1534,"edit":{"startOffset":1459,"stopOffset":1534,"replacement":"by (hoare_rule HoarePartial.ProcRec1) (vcg spec=modifies)","msg":null},"startOffset":1459,"severity":"Low","startPosition":"39:3","commands":[-6862,-6864,-6866]},{"name":"apply_isar_switch","stopPosition":"159:92","stopOffset":10453,"edit":null,"startOffset":10354,"severity":"Medium","startPosition":"158:1","commands":[-6952]},{"name":"complex_isar_initial_method","stopPosition":"265:62","stopOffset":15790,"edit":null,"startOffset":15742,"severity":"Medium","startPosition":"265:14","commands":[-7110]},{"name":"unrestricted_auto","stopPosition":"924:23","stopOffset":45224,"edit":null,"startOffset":45214,"severity":"High","startPosition":"924:13","commands":[-8216]},{"name":"unrestricted_auto","stopPosition":"952:21","stopOffset":46486,"edit":null,"startOffset":46476,"severity":"High","startPosition":"952:11","commands":[-8262]},{"name":"implicit_rule","stopPosition":"1011:21","stopOffset":48831,"edit":null,"startOffset":48827,"severity":"Medium","startPosition":"1011:17","commands":[-8384]},{"name":"implicit_rule","stopPosition":"1013:21","stopOffset":48874,"edit":null,"startOffset":48870,"severity":"Medium","startPosition":"1013:17","commands":[-8388]},{"name":"implicit_rule","stopPosition":"1018:21","stopOffset":49008,"edit":null,"startOffset":49004,"severity":"Medium","startPosition":"1018:17","commands":[-8398]},{"name":"unrestricted_auto","stopPosition":"1036:47","stopOffset":49727,"edit":null,"startOffset":49695,"severity":"High","startPosition":"1036:15","commands":[-8438]},{"name":"unrestricted_auto","stopPosition":"1038:25","stopOffset":49789,"edit":null,"startOffset":49779,"severity":"High","startPosition":"1038:15","commands":[-8442]},{"name":"unrestricted_auto","stopPosition":"1214:25","stopOffset":58019,"edit":null,"startOffset":58009,"severity":"High","startPosition":"1214:15","commands":[-8756]},{"name":"implicit_rule","stopPosition":"1308:27","stopOffset":62240,"edit":null,"startOffset":62236,"severity":"Medium","startPosition":"1308:23","commands":[-8956]},{"name":"implicit_rule","stopPosition":"1310:27","stopOffset":62295,"edit":null,"startOffset":62291,"severity":"Medium","startPosition":"1310:23","commands":[-8960]},{"name":"implicit_rule","stopPosition":"1315:27","stopOffset":62459,"edit":null,"startOffset":62455,"severity":"Medium","startPosition":"1315:23","commands":[-8970]},{"name":"apply_isar_switch","stopPosition":"1409:22","stopOffset":67009,"edit":null,"startOffset":67002,"severity":"Medium","startPosition":"1409:15","commands":[-9130]},{"name":"implicit_rule","stopPosition":"1578:27","stopOffset":75355,"edit":null,"startOffset":75351,"severity":"Medium","startPosition":"1578:23","commands":[-9504]},{"name":"implicit_rule","stopPosition":"1580:27","stopOffset":75410,"edit":null,"startOffset":75406,"severity":"Medium","startPosition":"1580:23","commands":[-9508]},{"name":"implicit_rule","stopPosition":"1585:27","stopOffset":75574,"edit":null,"startOffset":75570,"severity":"Medium","startPosition":"1585:23","commands":[-9518]},{"name":"apply_isar_switch","stopPosition":"1693:24","stopOffset":80747,"edit":null,"startOffset":80740,"severity":"Medium","startPosition":"1693:17","commands":[-9732]},{"name":"apply_isar_switch","stopPosition":"1955:24","stopOffset":94346,"edit":null,"startOffset":94339,"severity":"Medium","startPosition":"1955:17","commands":[-10324]},{"name":"implicit_rule","stopPosition":"2360:21","stopOffset":114988,"edit":null,"startOffset":114984,"severity":"Medium","startPosition":"2360:17","commands":[-11158]},{"name":"implicit_rule","stopPosition":"2362:21","stopOffset":115031,"edit":null,"startOffset":115027,"severity":"Medium","startPosition":"2362:17","commands":[-11162]},{"name":"implicit_rule","stopPosition":"2367:21","stopOffset":115165,"edit":null,"startOffset":115161,"severity":"Medium","startPosition":"2367:17","commands":[-11172]},{"name":"implicit_rule","stopPosition":"2377:21","stopOffset":115541,"edit":null,"startOffset":115537,"severity":"Medium","startPosition":"2377:17","commands":[-11188]},{"name":"implicit_rule","stopPosition":"2378:21","stopOffset":115562,"edit":null,"startOffset":115558,"severity":"Medium","startPosition":"2378:17","commands":[-11190]},{"name":"implicit_rule","stopPosition":"2382:21","stopOffset":115666,"edit":null,"startOffset":115662,"severity":"Medium","startPosition":"2382:17","commands":[-11198]},{"name":"apply_isar_switch","stopPosition":"2385:16","stopOffset":115746,"edit":null,"startOffset":115739,"severity":"Medium","startPosition":"2385:9","commands":[-11204]},{"name":"complex_isar_initial_method","stopPosition":"2785:57","stopOffset":133884,"edit":null,"startOffset":133847,"severity":"Medium","startPosition":"2785:20","commands":[-12064]},{"name":"apply_isar_switch","stopPosition":"2818:16","stopOffset":135180,"edit":null,"startOffset":135173,"severity":"Medium","startPosition":"2818:9","commands":[-12134]}]},"timing":237}]}
Loading

0 comments on commit 5aed1a3

Please sign in to comment.