Commit Graph

43 Commits

Author SHA1 Message Date
Cas Cremers
d56c2cafe6 Get rid of gcc __inline__ keywords.
Just let the compiler sort it out.
2019-01-04 14:15:38 +01:00
Cas Cremers
c256afc7ca Complex multiple interacting trampolines removal. 2018-11-05 14:43:00 +01:00
Cas Cremers
cdda26f21f Removed another trampoline; one of the type where omitting function argument types reduces warnings. Ouch. 2018-11-04 23:24:56 +01:00
Cas Cremers
92c5b0bedc Removed term_iterate_leaves. 2018-10-31 23:48:45 +01:00
Cas Cremers
fe1be9b3f0 Removing term_iterate_deVar, which is now obsolete. 2018-10-31 23:41:09 +01:00
Cas Cremers
a373667c23 Further underspecifying pointers helps to avoid warnings.
Alright, all checks now officially disabled :-(
2018-10-22 04:25:19 +02:00
Cas Cremers
85dbd20869 Stateful version of term leaves iterator. 2018-10-22 03:24:47 +02:00
Cas Cremers
fb3b13f4e3 Created initial stateful version of deVar iteration. 2018-10-22 03:18:52 +02:00
Cas Cremers
d06247fcfe Updating time stamps for next release. 2013-10-05 23:56:12 +01:00
Cas Cremers
7658644295 Rati Gelashvili reported a rare but annoying bug in the hash function handling.
The fix requires a significant reworking of the function handling. This
is a first attempt.

Conflicts:
	src/knowledge.c
	src/knowledge.h

Regression test suggests that the Hashfunction fix works.
2013-04-26 14:47:27 +02:00
Cas Cremers
1cbe9826ac Updated dates. 2012-04-24 13:56:51 +02:00
Cas Cremers
a03f06ea41 BUGFIX: Auto-claim naming scheme was context dependent.
The automatic mechanism to assign labels to claims was dependent on the
context. In practice, a claim could get a different label when analyzed in
isolation compared to when analyzed in parallel with some other protocols. This
caused problems for the multi-protocol analysis.
2011-01-27 14:12:51 +01:00
Cas Cremers
7d584cca1e Added GPL 2 License to the C sources.
A first step towards releasing Scyther completely to the public.
2007-06-11 14:01:04 +02:00
Cas Cremers
1542d65def - Big catchup commit to make sure we are up to beta7.
This includes a number of single patches, ranging from the vista fix with the buffers, to the start of many new minor features.
2007-05-18 14:06:29 +02:00
ccremers
91b52f6b4a - Removed more dead code, improved scantags.py 2007-01-27 11:07:45 +00:00
ccremers
8d66dc48fd - Fixed intruder generated value displays. 2006-12-05 10:10:17 +00:00
ccremers
1ce03104c5 Major:
- Added rho/sigma/constants fields to the runs, on which the new code is
  based. Over time, .locals should be deprecated in favour of these
  better variants.
- Untyped variant is out of grace for the time being (cf. Athena interm
  problems)
- Improved graph output further.

Minor:
- Added TERMLISTADD and APPEND macros for more concise code.
2006-03-15 21:30:19 +00:00
ccremers
2280187b32 - Improved dot class output. 2006-03-08 15:12:58 +00:00
ccremers
cf832ca1b1 - Seems to work again, but further testing is needed. 2006-02-27 22:27:09 +00:00
ccremers
b49d13b6ee - [[[ Broken commit. ]]]
Stuff seems to be working again, slightly less efficient though (count
  states).
2006-02-27 16:08:17 +00:00
ccremers
5d2d836d07 - Much work for the skeleton of the Hidelevel lemma. 2006-02-21 20:29:05 +00:00
ccremers
da75862d82 - Huge code documentation effort. 2006-01-02 21:06:08 +00:00
ccremers
e6505a72a3 - Further refactoring.
- Some cleanup.
2006-01-02 19:55:34 +00:00
ccremers
0505aaacd6 - New claim: CLAIM_Reachable
- Added new switches:
  -G,--generate-statespace
  -C,--generate-claims
- Claims are now allowed to have no label (they will be generated
  automatically)
- Output summary shows parameter of claims
- Internally, new symbols can now be generated by
  symbolNextFree(prefixsymbol)
2005-12-28 11:50:17 +00:00
ccremers
76666404b0 - Added '--concrete' switch to fill in to pick readable names for
variables.
2005-11-12 21:13:00 +00:00
ccremers
8b51593cf5 - Each attack now includes
* Initial knowledge
  * Role definitions for protocols involved
2005-05-12 14:52:50 +00:00
ccremers
820c2caed8 - Revisited type matching conditions.
- Introduced tuple unfolding stuff for Arachne. -m2 should work now.
2005-01-14 18:18:40 +00:00
ccremers
54ccd5179e - Added a new selector that picks goals that are local variables. 2004-12-29 16:05:32 +00:00
ccremers
a38925c9c2 - Added some useful macros to term.h to address subparts (e.g.
TermOp1(t)). Renamed all uses.
2004-11-16 12:06:36 +00:00
ccremers
b6af2f9dac - First try for diff function. 2004-11-01 14:06:26 +00:00
ccremers
0de3320009 - Fixed a memory leak in termLocal. This did not cause any problems for
the modelchecker, as it calls it only once, but it caused major
  problems for the arachne engine, which creates and destroys semiruns
  all the time.
2004-10-12 15:12:20 +00:00
ccremers
d58fc5ab43 - Made the label naming unique, by adding tuple info with the protocol
name. Now, we can simply test multiple protocol names by
  concatenation.
- Removed the pointer equality leaf hypothesis, as it didn't hold
  anymore.
2004-08-27 10:08:03 +00:00
ccremers
0fc008fe33 - Added keylevels to symbols. This is to help pruning the proofs, for
terms and patterns that do not originate on regular nodes.
2004-08-20 19:16:56 +00:00
ccremers
f25f0abd4e - Fixed a memory error. 2004-08-19 14:49:03 +00:00
ccremers
b2d21f0a8a BROKEN
- Working on new algorithm. Some memory error can occur.
2004-08-18 14:06:14 +00:00
ccremers
c5695d6fe8 - Added more generic term iterators. 2004-08-18 12:12:29 +00:00
ccremers
bb78c71c90 - Introduced termInTerm (bigterm, smallterm) 2004-08-17 14:11:25 +00:00
ccremers
74851e0393 - Consistency improvements. 2004-08-14 14:27:46 +00:00
ccremers
f219461c8d - After some trouble, nonce binding is working nicely. 2004-08-14 14:23:21 +00:00
ccremers
0f470cf6a2 - Rewrote roleInstance to cope with Arachne needs.
- Introduced some iterators for e.g. term leaves and roledefs. These are
  not used everywhere yet.
2004-08-12 09:14:31 +00:00
ccremers
71c658051e - Reindented everything, so the layout is up to date again. 2004-08-09 10:05:58 +00:00
ccremers
b22667a791 - Fixed termlist printing. 2004-07-29 11:15:07 +00:00
ccremers
60b02eea0e - Renamed nearly all files. Now, we try to use singular terms.
Exception: states.h is the plural form.
2004-07-24 19:07:29 +00:00