Project

General

Profile

« Previous | Next » 

Revision 105b3645

Added by Guillaume Davy over 9 years ago

Delete tests files that have no k

View differences:

tests/gen_contracts.py
12 12
re_node = re.compile('.*node.*')
13 13
re_ensures = re.compile('.*ensures.*')
14 14
re_k = re.compile('--![ ]*k[ ]*:([^;]*);')
15
re_frama_res = re.compile('Proved goals:[ ]*([0-9]*)[ ]*/[ ]*([0-9]*)')
15 16

  
16 17
def findInLines(lines, regex):
17 18
	res = []
......
59 60
	properties = findInLines(lines, re_property)
60 61
	k = findInLines(lines, re_k)
61 62
	if k:
62
		return (None, "ALREADY", None)
63
		return (None, "ALREADY", "KEEP")
63 64
	if not properties:
64 65
		return (None, "NOPR", None)
65 66
	if len(properties) > 1:
......
68 69
	f = open(top, 'w')
69 70
	f.write("".join(lines))
70 71
	f.close()
71
	p = subprocess.Popen(["timeout", "40", "pkind", top, "-timeout", str(TIMEOUT), "-k_incremental", str(MAX)], stdout=subprocess.PIPE, stderr=subprocess.PIPE)
72
	p = subprocess.Popen(["timeout", "10", "pkind", top, "-timeout", str(TIMEOUT), "-k_incremental", str(MAX)], stdout=subprocess.PIPE, stderr=subprocess.PIPE)
72 73
	(stdout, stderr) = p.communicate()
73 74
	try:
74 75
		root = ET.fromstring(stdout)
75 76
	except ET.ParseError:
76 77
		return (None, "TIMEOUT", None)
78
	answer = root.find(".//Answer")
79
	if answer is None:
80
		return (None, "NO_ANS", None)
81
	if answer.text != "valid":
82
		return (None, "INVALID", None)
77 83
	k = root.find(".//K")
78 84
	if k is None:
79
		return (None, "ERR", None)
85
		return (None, "NO_K", None)
80 86
	try:
81 87
		k = int(k.text)
82 88
	except ValueError:
83 89
		return (None, "NOTPROVED", None)
84 90
	lines.insert(properties[0][0], "--!k:{};\n".format(k))
85
	return (lines, "OK("+"k=" + str(k)+")", None)
91
	return (lines, "OK("+"k=" + str(k)+")", "KEEP")
86 92

  
87 93
def compileLustre(lines, temp):
88 94
	top = temp + "/top.lus"
......
93 99
	(stdout, stderr) = p.communicate()
94 100
	res = p.wait()
95 101
	if res != 0:
96
		return (None, "ERR_"+str(res), stdout+"\n-------\n"+stderr)
102
		return (None, "ERR_"+str(res), None)
97 103
	return (lines, "OK", None)
98 104

  
99

  
100

  
101 105
def framac(lines, temp):
102
	FRAMAC=["frama-c", "-wp", "-wp-prover", "CVC4,alt-ergo,z3,coq", temp+"/top.c", "-wp-par", "2", "-wp-rte", "-wp-model", "ref", """-wp-tactic="Require Why3. intros. hnf. repeat split;try why3 \"CVC3\" timelimit 10;try why3 \"Z3\" timelimit 10;why3 \"CVC4\" timelimit 10""", "-wp-script", temp+"/top.coq" "-wp-no-let"]
106
	FRAMAC=["frama-c", temp+"/top.c"]
103 107
	p = subprocess.Popen(FRAMAC, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
104 108
	(stdout, stderr) = p.communicate()
105 109
	res = p.wait()
106 110
	if res != 0:
107
		return (None, "ERR_"+str(res), temp+"\n"+stdout+"\n-------\n"+stderr)
108
	return (lines, "OK", stdout)
111
		return (None, "PARSE_"+str(res), None)
112
	FRAMAC=["frama-c", "-wp", "-wp-prover", "CVC4,alt-ergo,z3,coq", temp+"/top.c", "-wp-par", "2", "-wp-model", "ref", """-wp-tactic="Require Why3. intros. hnf. repeat split;try why3 \"CVC3\" timelimit 10;try why3 \"Z3\" timelimit 10;why3 \"CVC4\" timelimit 10" """, "-wp-script", temp+"/top.coq", "-wp-no-let"]
113
	#"-wp-rte", 
114
	p = subprocess.Popen(FRAMAC, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
115
	(stdout, stderr) = p.communicate()
116
	res = p.wait()
117
	if res != 0:
118
		return (None, "ERR_"+str(res), None)
119
	m = re_frama_res.search(stdout)
120
	if not m:
121
		return (None, "BAD_OUT", None)
122
	return (lines, str(m.group(1))+"/"+str(m.group(2)), None)
109 123

  
110 124

  
111
def parseFile(inp, out, todo):
125
def parseFile(inp, todo):
112 126
	lines = inp.readlines()
113 127
	
114 128
	temp = tempfile.mkdtemp(prefix="contracts_")
115 129
	res = ""
116
	dats = []
130
	data = None
131
	ok = False
117 132
	for f in todo:
118 133
		x = [[]]
119
		(newlines, r, data) = f(lines[:], temp)
120
		res += "{:10} ".format(r[:10])
134
		(newlines, r, cmd) = f(lines[:], temp)
135
		res += "{:8} ".format(r[:8])
121 136
		if newlines:
122 137
			lines = newlines
123
		if data:
124
			dats.append(data)
125
	out.write("".join(lines))
138
		if cmd == "STOP":
139
			break
140
		if cmd == "KEEP":
141
			ok = True
142
	if ok:
143
		res += "WRITE"
144
		data = "".join(lines)
126 145
	shutil.rmtree(temp)
127 146
	
128
	return (res, dats)
147
	return (res, data)
129 148

  
130
TODO=[modProperties, addEnsures, addK, compileLustre]
149
TODO=[modProperties, addEnsures, addK, compileLustre, framac]
131 150

  
132
LENGTH=50
151
LENGTH=40
133 152

  
134 153
target="./generated/"
135 154

  
136
#if os.path.exists(target):
137
#	shutil.rmtree(target)
155
if os.path.exists(target):
156
	shutil.rmtree(target)
138 157

  
139
orig = "/home/davyg/good"
158
orig = "tests_new"
140 159
for root, dirs, files in os.walk(orig):
141 160
	short = root[len(orig):]
142 161
	os.mkdir(target+"/"+short)
......
144 163
		if not x.endswith(".lus"):
145 164
			continue
146 165
		inp = open(root+"/"+x, "r")
147
		out = open(target+"/"+short+"/"+x, "w")
148
		(res, dats) = parseFile(inp, out, TODO)
166
		(res, data) = parseFile(inp, TODO)
149 167
		inp.close()
150
		out.close()
168
		if data:
169
			out = open(target+"/"+short+"/"+x, "w")
170
			out.write(data)
171
			out.close()
151 172
		print(("Process {0:"+str(LENGTH)+"} : {1}").format(("./"+short+"/"+x)[:LENGTH], res))
152
		if dats:
153
			print("\n/////////////////////\n".join(dats))
154 173
		sys.stdout.flush()

Also available in: Unified diff