Log of /branches

---

Revision 103351 - Directory Listing
Modified Tue Jul 23 15:14:02 2019 UTC (4 months, 2 weeks ago) by manus

Merged 103348, 103349 and 103350 from trunk

---

Revision 103187 - Directory Listing
Modified Mon May 20 18:27:52 2019 UTC (6 months, 3 weeks ago) by jfiat

Merged from trunk 103185 and 103186.

---

Revision 103184 - Directory Listing
Modified Mon May 20 15:05:24 2019 UTC (6 months, 3 weeks ago) by jfiat

Merged from trunk revisions 103181..103183 .

---

Revision 103180 - Directory Listing
Modified Sat May 18 16:19:53 2019 UTC (6 months, 3 weeks ago) by jfiat

Merge revisions 103179, 103178 from trunk.

---

Revision 103176 - Directory Listing
Modified Fri May 17 14:17:30 2019 UTC (6 months, 3 weeks ago) by jfiat

Updated to EiffelStudio 19.05 release.

---

Revision 103175 - Directory Listing
Modified Fri May 17 13:50:00 2019 UTC (6 months, 3 weeks ago) by jfiat

Merged revisions 103167-103174 from trunk.

---

Revision 103167 - Directory Listing
Modified Thu May 16 10:50:11 2019 UTC (6 months, 3 weeks ago) by jfiat

Version 19.05 Release.

---

Revision 102589 - Directory Listing
Modified Thu Dec 13 06:30:09 2018 UTC (11 months, 4 weeks ago) by manus

Updated to EiffelStudio 18.11 Release

---

Revision 102568 - Directory Listing
Modified Fri Dec 7 15:46:09 2018 UTC (12 months ago) by manus

Version 18.11 Release

---

Revision 101985 - Directory Listing
Modified Sun Jul 22 18:49:14 2018 UTC (16 months, 2 weeks ago) by alexk

Updated syntax.

---

Revision 101984 - Directory Listing
Modified Sun Jul 22 18:48:01 2018 UTC (16 months, 2 weeks ago) by alexk

Updated to a more recent version of Gobo.

---

Revision 101972 - Directory Listing
Modified Thu Jul 12 21:22:47 2018 UTC (16 months, 4 weeks ago) by manus

New CD key for 18.07

---

Revision 101967 - Directory Listing
Modified Mon Jul 9 15:52:33 2018 UTC (17 months ago) by jfiat

Merged /trunk/ up to revision 101966 in Eiffel_18.07 branch.

---

Revision 101959 - Directory Listing
Modified Mon Jul 9 11:42:23 2018 UTC (17 months ago) by jfiat

Merged /trunk/ up to revision 101958 in Eiffel_18.07 branch.

---

Revision 101918 - Directory Listing
Modified Thu Jul 5 14:44:28 2018 UTC (17 months ago) by jfiat

Merged /trunk/ up to revision 101917 and switch to Eiffel_18.07 branch.

---

Revision 101917 - Directory Listing
Modified Thu Jul 5 08:39:32 2018 UTC (17 months ago) by jfiat

Moved to 18.07

---

Revision 101819 - Directory Listing
Modified Fri Jun 8 14:37:29 2018 UTC (18 months ago) by manus

Revert to correct version number

---

Revision 101817 - Directory Listing
Modified Mon Jun 4 14:27:57 2018 UTC (18 months, 1 week ago) by manus

Fixed files that should not have been modified

---

Revision 101816 - Directory Listing
Modified Mon Jun 4 14:22:39 2018 UTC (18 months, 1 week ago) by manus

CD key for enterprise/eval install of EiffelStudio 18.05

---

Revision 101812 - Directory Listing
Modified Mon Jun 4 14:10:58 2018 UTC (18 months, 1 week ago) by manus

Updated path for 18.05 checkout

---

Revision 101811 - Directory Listing
Modified Mon Jun 4 14:06:48 2018 UTC (18 months, 1 week ago) by manus

Merged /trunk/Src:r101803-101810

---

Revision 101803 - Directory Listing
Modified Tue May 29 14:47:23 2018 UTC (18 months, 1 week ago) by manus

Merge from trunk rev#101801

---

Revision 101800 - Directory Listing
Modified Tue May 29 04:00:18 2018 UTC (18 months, 1 week ago) by manus

Fixed Eiffel 18.05 GUIDs 

---

Revision 101798 - Directory Listing
Modified Tue May 29 03:25:38 2018 UTC (18 months, 1 week ago) by manus

New 18.05 Release

---

Revision 101423 - Directory Listing
Modified Wed Feb 14 04:06:43 2018 UTC (21 months, 3 weeks ago) by manus

Add CD key for enterprise/eval install

---

Revision 101419 - Directory Listing
Modified Wed Feb 14 03:44:09 2018 UTC (21 months, 3 weeks ago) by manus

Merge changes from master up to rev#101418

---

Revision 101361 - Directory Listing
Modified Mon Feb 5 15:52:50 2018 UTC (22 months ago) by manus

Update path for 18.01 release

---

Revision 101359 - Directory Listing
Modified Mon Feb 5 15:36:40 2018 UTC (22 months ago) by manus

Creation of EiffelStudio 18.01 branch

---

Revision 100414 - Directory Listing
Modified Thu May 18 04:46:48 2017 UTC (2 years, 6 months ago) by manus

Use egcc and e++ instead of gcc and g++

Due to the default version of gcc being quite old, we use the latest version which is named egcc and eg++ on OpenBSD.

---

Revision 100412 - Directory Listing
Modified Thu May 18 04:35:54 2017 UTC (2 years, 6 months ago) by manus

Merged rev#100411 from trunk

---

Revision 100409 - Directory Listing
Modified Wed May 17 16:09:31 2017 UTC (2 years, 6 months ago) by manus

Merged changes from trunk from rev#100400-100404 and rev#100406-100408

---

Revision 100395 - Directory Listing
Modified Sun May 14 04:21:09 2017 UTC (2 years, 6 months ago) by manus

Use Eiffel_17.05 branch

---

Revision 100394 - Directory Listing
Modified Sun May 14 04:18:50 2017 UTC (2 years, 6 months ago) by manus

Use Eiffel_17.05 branch

---

Revision 100393 - Directory Listing
Modified Sun May 14 04:15:07 2017 UTC (2 years, 6 months ago) by manus

Added CD key for 17.05 release

---

Revision 100392 - Directory Listing
Modified Sun May 14 04:04:36 2017 UTC (2 years, 6 months ago) by manus

Created EiffelStudio 17.05 release

---

Revision 100266 - Directory Listing
Modified Fri Apr 28 18:48:36 2017 UTC (2 years, 7 months ago) by manus

Fixed non-C local declaration

---

Revision 100265 - Directory Listing
Modified Fri Apr 28 18:42:35 2017 UTC (2 years, 7 months ago) by manus

Merge rev#100264: Fix retrieval of old routine objects

---

Revision 99724 - Directory Listing
Modified Fri Jan 13 17:16:16 2017 UTC (2 years, 10 months ago) by manus

Merge rev#99721, rev#99722 and rev#99723 from trunk

For Iron.

---

Revision 99697 - Directory Listing
Modified Tue Jan 3 17:57:19 2017 UTC (2 years, 11 months ago) by manus

Updated to the 17.01 release branch

---

Revision 99696 - Directory Listing
Modified Tue Jan 3 17:54:05 2017 UTC (2 years, 11 months ago) by manus

Updated to 17.01 release branch

---

Revision 99694 - Directory Listing
Modified Tue Jan 3 17:50:20 2017 UTC (2 years, 11 months ago) by manus

Created EiffelStudio 17.01 release branch

---

Revision 99391 - Directory Listing
Modified Sat Nov 5 05:48:03 2016 UTC (3 years, 1 month ago) by manus

Fix bug#19284 causing a wrong runtime behavior on platforms without atomic operations

We only need the & to create the lock, but whenever we use it we should not provide the &.

---

Revision 99058 - Directory Listing
Modified Wed Jul 27 14:07:57 2016 UTC (3 years, 4 months ago) by manus

Cleanup from previous build

---

Revision 99057 - Directory Listing
Modified Tue Jul 26 22:53:03 2016 UTC (3 years, 4 months ago) by manus

Disable call to `eif_show_console` in `console_def` while waiting for the Eiffel code to be updated to take into account this change. This might break some process redirection scenarios which we just fixed.

---

Revision 99053 - Directory Listing
Modified Sat Jul 23 13:24:01 2016 UTC (3 years, 4 months ago) by manus

Merge rev#99043, rev#99044 and rev#99050.

---

Revision 98966 - Directory Listing
Modified Wed Jun 29 12:58:45 2016 UTC (3 years, 5 months ago) by manus

Merged /trunk/Src:r98845,98857,98860,98864,98901-98905,98918,98924,98942,98945,98951-98952,98964

---

Revision 98898 - Directory Listing
Modified Thu Jun 9 12:30:02 2016 UTC (3 years, 6 months ago) by manus

Add 16.05 CD Key

---

Revision 98812 - Directory Listing
Modified Thu May 19 14:16:26 2016 UTC (3 years, 6 months ago) by manus

Updated to the EiffelStudio 16.05 branch

---

Revision 98809 - Directory Listing
Modified Thu May 19 13:51:21 2016 UTC (3 years, 6 months ago) by manus

Updated to the EiffelStudio 16.05 branch

---

Revision 98806 - Directory Listing
Modified Thu May 19 13:35:29 2016 UTC (3 years, 6 months ago) by manus

New EiffelStudio 16.05 release branch

---

Revision 98493 - Directory Listing
Modified Sun Feb 7 05:19:00 2016 UTC (3 years, 10 months ago) by manus

Merging r98491,98492 from trunk.

---

Revision 98464 - Directory Listing
Modified Tue Feb 2 13:53:12 2016 UTC (3 years, 10 months ago) by manus

Merging r98309-98311,98313,98316,98343,98388,98406,98457 from trunk.

---

Revision 98312 - Directory Listing
Modified Tue Dec 22 13:53:15 2015 UTC (3 years, 11 months ago) by evemerge

Partial merge from trunk#98292.
SVN tree conflicts and regular conflicts have been resolved,
but some compilation errors in EVE still exist.

---

Revision 98307 - Directory Listing
Modified Mon Dec 21 13:32:05 2015 UTC (3 years, 11 months ago) by manus

Updated to the EiffelStudio 15.12 branch.

---

Revision 98304 - Directory Listing
Modified Mon Dec 21 13:21:24 2015 UTC (3 years, 11 months ago) by manus

Updated to the EiffelStudio 15.12 branch.

---

Revision 98302 - Directory Listing
Modified Mon Dec 21 13:08:30 2015 UTC (3 years, 11 months ago) by manus

New EiffelStudio 15.12 release

---

Revision 98291 - Directory Listing
Modified Fri Dec 18 15:51:59 2015 UTC (3 years, 11 months ago) by evemerge

Moved the directory code_analysis/abstract/cfg one level up to code_analysis/cfg to avoid tree conflicts with trunk.

---

Revision 98134 - Directory Listing
Modified Mon Nov 23 11:59:42 2015 UTC (4 years ago) by trudelm

updated test

---

Revision 98133 - Directory Listing
Modified Mon Nov 23 07:04:29 2015 UTC (4 years ago) by varivera

Checking the graph based implementation of Alias Calculus: new test added

---

Revision 98127 - Directory Listing
Modified Fri Nov 20 15:49:14 2015 UTC (4 years ago) by trudelm

extended alias analysis implementation

---

Revision 98125 - Directory Listing
Modified Fri Nov 20 12:11:03 2015 UTC (4 years ago) by varivera

Adding a test for the Graph Based Alias analysis

---

Revision 98123 - Directory Listing
Modified Fri Nov 20 10:27:31 2015 UTC (4 years ago) by maxpei

Added the missing file.

---

Revision 98122 - Directory Listing
Modified Fri Nov 20 09:50:09 2015 UTC (4 years ago) by varivera

deleting old_changeC folder

---

Revision 98121 - Directory Listing
Modified Fri Nov 20 09:46:10 2015 UTC (4 years ago) by varivera

adding old files Alias-change Calculi

---

Revision 98119 - Directory Listing
Modified Thu Nov 19 15:10:50 2015 UTC (4 years ago) by trudelm

replaced relational representation with graph based one

---

Revision 98118 - Directory Listing
Modified Thu Nov 19 13:59:02 2015 UTC (4 years ago) by maxpei

Fixed a fault in AutoFix. Due to the fault, violated contract expression may not be used as a fixing target.

---

Revision 98082 - Directory Listing
Modified Fri Nov 6 00:44:40 2015 UTC (4 years, 1 month ago) by evemerge

<<Merged from trunk#98081.>>

---

Revision 98080 - Directory Listing
Modified Thu Nov 5 12:10:42 2015 UTC (4 years, 1 month ago) by evemerge

<<Merged from trunk#98079.>>
Applied rev#98062 at the right place.
Marked {ANY}.set_handler_active/passive as obsolete
and removed their implementation.

---

Revision 98050 - Directory Listing
Modified Fri Oct 30 00:55:56 2015 UTC (4 years, 1 month ago) by evemerge

<<Merged from trunk#98049.>>

---

Revision 98041 - Directory Listing
Modified Fri Oct 23 00:19:23 2015 UTC (4 years, 1 month ago) by evemerge

<<Merged from trunk#98040.>>

---

Revision 98002 - Directory Listing
Modified Thu Oct 15 23:51:31 2015 UTC (4 years, 1 month ago) by evemerge

<<Merged from trunk#98001.>>

---

Revision 97972 - Directory Listing
Modified Thu Oct 8 23:47:26 2015 UTC (4 years, 2 months ago) by evemerge

<<Merged from trunk#97971.>>

---

Revision 97970 - Directory Listing
Modified Thu Oct 8 14:06:14 2015 UTC (4 years, 2 months ago) by maxpei

Fix a bug in AutoFix. So in case of no failing tests in the input, AutoFix will exit gracefully.

---

Revision 97969 - Directory Listing
Modified Thu Oct 8 14:01:08 2015 UTC (4 years, 2 months ago) by maxpei

Added exception tag to the fault signature id so that it becomes more descriptive.

---

Revision 97968 - Directory Listing
Modified Thu Oct 8 13:57:17 2015 UTC (4 years, 2 months ago) by maxpei

Fixed a bug in the interpretation of execution trace in AutoFix.

---

Revision 97955 - Directory Listing
Modified Mon Oct 5 13:51:30 2015 UTC (4 years, 2 months ago) by manus

Fixed invalid CD key for 15.08 installation.

---

Revision 97954 - Directory Listing
Modified Mon Oct 5 13:07:24 2015 UTC (4 years, 2 months ago) by maxpei

Added logging of intermediate info to AutoFix;
Added support for 'Unmatched inspect value' exception type to AutoTest.

---

Revision 97952 - Directory Listing
Modified Thu Oct 1 23:44:19 2015 UTC (4 years, 2 months ago) by evemerge

<<Merged from trunk#97951.>>

---

Revision 97927 - Directory Listing
Modified Thu Sep 24 23:49:24 2015 UTC (4 years, 2 months ago) by evemerge

<<Merged from trunk#97926.>>

---

Revision 97918 - Directory Listing
Modified Thu Sep 17 10:36:10 2015 UTC (4 years, 2 months ago) by evemerge

<<Merged from trunk#97917.>>

---

Revision 97875 - Directory Listing
Modified Fri Aug 21 00:31:20 2015 UTC (4 years, 3 months ago) by evemerge

<<Merged from trunk#97873.>>

---

Revision 97865 - Directory Listing
Modified Wed Aug 19 23:53:56 2015 UTC (4 years, 3 months ago) by manus

Merged from trunk: 
Fixed obsolete calls to `attempt' which is now called `attempted'.

---

Revision 97861 - Directory Listing
Modified Wed Aug 19 21:38:53 2015 UTC (4 years, 3 months ago) by manus

Committed temporary workaround in 15.08 release for SCOOP because `{ANY}.generating_type' is not SCOOP safe at the time being.

---

Revision 97855 - Directory Listing
Modified Wed Aug 19 21:00:29 2015 UTC (4 years, 3 months ago) by manus

Updating to check out 15.08 branch.

---

Revision 97854 - Directory Listing
Modified Wed Aug 19 19:40:54 2015 UTC (4 years, 3 months ago) by manus

Created 15.08 Release Branch

---

Revision 97816 - Directory Listing
Modified Fri Aug 14 00:26:44 2015 UTC (4 years, 3 months ago) by evemerge

<<Merged from trunk#97815.>>

---

Revision 97812 - Directory Listing
Modified Thu Aug 13 14:11:38 2015 UTC (4 years, 3 months ago) by maxpei

Fixed a bug in the precondition satisfaction strategy of AutoTest.
Problem: when there are many predicates to satisfy and each has many candidates, the time to try out all the combinations is prohibitively long.
Fix: limit the maximum number of combinations examined.

---

Revision 97797 - Directory Listing
Modified Mon Aug 10 09:49:53 2015 UTC (4 years, 4 months ago) by maxpei

Fix a bug: when feature-invalid-test-case-rate for a feature is accessed for the first time, the feature is not in the hashtable yet, which causes a precondition violation.

---

Revision 97794 - Directory Listing
Modified Fri Aug 7 00:12:27 2015 UTC (4 years, 4 months ago) by evemerge

<<Merged from trunk#97793.>>

---

Revision 97761 - Directory Listing
Modified Fri Jul 31 12:39:33 2015 UTC (4 years, 4 months ago) by maxpei

Fixed the bug where provisional syntax elements causing eiffel parsers used in AutoTest to fail.

---

Revision 97760 - Directory Listing
Modified Fri Jul 31 00:23:16 2015 UTC (4 years, 4 months ago) by evemerge

<<Merged from trunk#97759.>>

---

Revision 97759 - Directory Listing
Modified Thu Jul 30 15:24:18 2015 UTC (4 years, 4 months ago) by maxpei

Fixed the bug where marks (e.g. !, ?, attached, detachable, and separate) in type strings are not recognized by the parser, and causing problems in test generation.

---

Revision 97755 - Directory Listing
Modified Fri Jul 24 00:50:00 2015 UTC (4 years, 4 months ago) by evemerge

<<Merged from trunk#97754.>>

---

Revision 97733 - Directory Listing
Modified Fri Jul 17 00:08:53 2015 UTC (4 years, 4 months ago) by evemerge

<<Merged from trunk#97732.>>

---

Revision 97695 - Directory Listing
Modified Mon Jul 13 12:10:53 2015 UTC (4 years, 4 months ago) by gabriel-fallen

First version of change specification inference.
CHANGE_SPEC_ANALYZER_ON_RELATION is inherited from CHANGE_ANALYZER_ON_RELATION.
ALIAS_ANALYZER_ON_RELATION is modified (in process_bin_eq_as) to walk over expanded types.

---

Revision 97683 - Directory Listing
Modified Fri Jul 10 00:36:42 2015 UTC (4 years, 5 months ago) by evemerge

<<Merged from trunk#97682.>>

---

Revision 97640 - Directory Listing
Modified Fri Jul 3 14:29:40 2015 UTC (4 years, 5 months ago) by varivera

Alias Analysis test added

---

Revision 97637 - Directory Listing
Modified Fri Jul 3 14:16:04 2015 UTC (4 years, 5 months ago) by varivera

Alias Analysis test added

---

Revision 97631 - Directory Listing
Modified Fri Jul 3 08:36:31 2015 UTC (4 years, 5 months ago) by evemerge

<<Merged from trunk#97626.>>

---

Revision 97574 - Directory Listing
Modified Fri Jun 26 09:50:36 2015 UTC (4 years, 5 months ago) by evemerge

<<Merged from trunk#97569.>>

---

Revision 97509 - Directory Listing
Modified Fri Jun 19 00:51:54 2015 UTC (4 years, 5 months ago) by evemerge

<<Merged from trunk#97508.>>

---

Revision 97487 - Directory Listing
Modified Thu Jun 18 14:41:11 2015 UTC (4 years, 5 months ago) by romanschmocker

Moved the scoop_patterns library to trunk.

---

Revision 97482 - Directory Listing
Modified Thu Jun 18 08:19:50 2015 UTC (4 years, 5 months ago) by romanschmocker

Changed CP_EVENT to be able to handle Void tuples.
Changed the interface of CP_PROMISE: Now there's only one
change event without arguments, which makes sure that no
lock passing can happen.

---

Revision 97481 - Directory Listing
Modified Wed Jun 17 17:15:06 2015 UTC (4 years, 5 months ago) by trudelm

Alias analysis: AST viewer now also shows the source code.

---

Revision 97477 - Directory Listing
Modified Tue Jun 16 15:55:31 2015 UTC (4 years, 5 months ago) by trudelm

Alias analysis: Added a general purpose AST viewer for inspecting/understanding the AST.

---

Revision 97464 - Directory Listing
Modified Thu Jun 11 23:50:45 2015 UTC (4 years, 6 months ago) by evemerge

<<Merged from trunk#97463.>>

---

Revision 97460 - Directory Listing
Modified Thu Jun 11 12:57:55 2015 UTC (4 years, 6 months ago) by trudelm

Alias analysis: improved test suite GUI

---

Revision 97459 - Directory Listing
Modified Thu Jun 11 12:44:12 2015 UTC (4 years, 6 months ago) by trudelm

Alias analysis: added statistics to the test suite

---

Revision 97448 - Directory Listing
Modified Tue Jun 9 15:23:27 2015 UTC (4 years, 6 months ago) by evemerge

<<Merged from trunk#97447.>>

---

Revision 97444 - Directory Listing
Modified Tue Jun 9 13:03:56 2015 UTC (4 years, 6 months ago) by trudelm

Alias analysis: disabled word wrapping in GUI

---

Revision 97443 - Directory Listing
Modified Tue Jun 9 13:00:28 2015 UTC (4 years, 6 months ago) by trudelm

Alias analysis: added tests

---

Revision 97442 - Directory Listing
Modified Tue Jun 9 12:27:41 2015 UTC (4 years, 6 months ago) by trudelm

Alias analysis: fixed test AAT_BASIC.test_locals

---

Revision 97427 - Directory Listing
Modified Fri Jun 5 08:11:31 2015 UTC (4 years, 6 months ago) by evemerge

<<Merged from trunk#97426.>>

---

Revision 97404 - Directory Listing
Modified Fri May 29 10:41:03 2015 UTC (4 years, 6 months ago) by trudelm

added a test from Victor

---

Revision 97403 - Directory Listing
Modified Fri May 29 10:22:04 2015 UTC (4 years, 6 months ago) by trudelm

improved test suite

---

Revision 97390 - Directory Listing
Modified Fri May 29 04:06:51 2015 UTC (4 years, 6 months ago) by evemerge

<<Merged from trunk#97389.>>

---

Revision 97386 - Directory Listing
Modified Thu May 28 08:54:52 2015 UTC (4 years, 6 months ago) by evemerge

<<Merged from trunk#97385.>>

---

Revision 97385 - Directory Listing
Modified Wed May 27 15:22:34 2015 UTC (4 years, 6 months ago) by trudelm

Alias analysis: added tests

---

Revision 97384 - Directory Listing
Modified Wed May 27 14:45:55 2015 UTC (4 years, 6 months ago) by trudelm

Alias analysis: added a test for local variables

---

Revision 97338 - Directory Listing
Modified Fri May 22 04:08:15 2015 UTC (4 years, 6 months ago) by evemerge

<<Merged from trunk#97337.>>

---

Revision 97335 - Directory Listing
Modified Thu May 21 13:03:36 2015 UTC (4 years, 6 months ago) by trudelm

Alias analysis: small GUI improvements

---

Revision 97334 - Directory Listing
Modified Thu May 21 12:32:21 2015 UTC (4 years, 6 months ago) by trudelm

Alias analysis: added a test suite

---

Revision 97290 - Directory Listing
Modified Fri May 15 03:45:01 2015 UTC (4 years, 6 months ago) by evemerge

<<Merged from trunk#97289.>>

---

Revision 97271 - Directory Listing
Modified Mon May 11 11:42:24 2015 UTC (4 years, 7 months ago) by evemerge

<<Merged from trunk#97269.>>
Added stub implementations for process_separate_b in E2B_VISITOR and JSC_VISITOR.

---

Revision 97269 - Directory Listing
Modified Mon May 11 09:10:49 2015 UTC (4 years, 7 months ago) by trudelm

inheritance fixlet

---

Revision 97241 - Directory Listing
Modified Tue May 5 15:16:59 2015 UTC (4 years, 7 months ago) by trudelm

Alias analysis: showing status after stepping

---

Revision 97165 - Directory Listing
Modified Fri Apr 24 04:10:39 2015 UTC (4 years, 7 months ago) by evemerge

<<Merged from trunk#97164.>>

---

Revision 97136 - Directory Listing
Modified Mon Apr 20 11:48:57 2015 UTC (4 years, 7 months ago) by trudelm

Alias analysis: moved console toolbar to console tab

---

Revision 97135 - Directory Listing
Modified Mon Apr 20 10:38:53 2015 UTC (4 years, 7 months ago) by trudelm

Alias analysis: removed debugging breakpoint menus/behavior

---

Revision 97123 - Directory Listing
Modified Fri Apr 17 16:29:51 2015 UTC (4 years, 7 months ago) by trudelm

Alias analysis: scroll code when stepping

---

Revision 97121 - Directory Listing
Modified Fri Apr 17 15:54:19 2015 UTC (4 years, 7 months ago) by trudelm

Alias analysis: added GUI skeleton

---

Revision 97110 - Directory Listing
Modified Fri Apr 17 09:20:04 2015 UTC (4 years, 7 months ago) by evemerge

<<Merged from trunk#97108.>>

---

Revision 97103 - Directory Listing
Modified Wed Apr 15 12:46:38 2015 UTC (4 years, 7 months ago) by trudelm

Alias analysis: changed to relation based representation

---

Revision 97056 - Directory Listing
Modified Fri Apr 10 03:50:13 2015 UTC (4 years, 8 months ago) by evemerge

<<Merged from trunk#97055.>>

---

Revision 97037 - Directory Listing
Modified Tue Apr 7 10:17:00 2015 UTC (4 years, 8 months ago) by evemerge

<<Merged from trunk#97035.>>

---

Revision 96927 - Directory Listing
Modified Fri Mar 27 13:39:18 2015 UTC (4 years, 8 months ago) by evemerge

<<Merged from trunk#96918.>>

---

Revision 96904 - Directory Listing
Modified Wed Mar 25 09:35:07 2015 UTC (4 years, 8 months ago) by schmisam

Fixed a bug in rule #7 with types containing formal generics.

---

Revision 96899 - Directory Listing
Modified Mon Mar 23 06:33:48 2015 UTC (4 years, 8 months ago) by schmisam

Added vision2 library to tests for final testing.

---

Revision 96898 - Directory Listing
Modified Mon Mar 23 04:46:24 2015 UTC (4 years, 8 months ago) by schmisam

Reformulation of violation messages. Handling of special cases with conform_to

---

Revision 96897 - Directory Listing
Modified Mon Mar 23 04:41:13 2015 UTC (4 years, 8 months ago) by schmisam

Code cleanup.

---

Revision 96896 - Directory Listing
Modified Mon Mar 23 03:09:39 2015 UTC (4 years, 8 months ago) by schmisam

Changed .node_type calls to account for void types.

---

Revision 96895 - Directory Listing
Modified Sun Mar 22 17:38:33 2015 UTC (4 years, 8 months ago) by schmisam

Adjusted properties.

---

Revision 96894 - Directory Listing
Modified Sun Mar 22 17:36:50 2015 UTC (4 years, 8 months ago) by schmisam

Changed .ecf file to ignore tests

---

Revision 96893 - Directory Listing
Modified Sun Mar 22 01:07:56 2015 UTC (4 years, 8 months ago) by schmisam

Deletion of accidental copy of rule.

---

Revision 96892 - Directory Listing
Modified Sun Mar 22 01:04:18 2015 UTC (4 years, 8 months ago) by schmisam

More cleanup of folders.
Added test case for debugging.

---

Revision 96891 - Directory Listing
Modified Sun Mar 22 00:18:08 2015 UTC (4 years, 8 months ago) by schmisam

Cleanup of folder hierarchy.

---

Revision 96890 - Directory Listing
Modified Sat Mar 21 05:47:55 2015 UTC (4 years, 8 months ago) by schmisam

Added rule #9.
Added rule #29.
Added fix for rule #9.
Added fix for rule #29.
Added fix for rule #7.
Fixed bug in CA_ALL_RULES_CHECKER with binary constructs not executing post actions.
Added bin_ne equation to ca_all_rules_checker.
Removed 009_useless_contract from tests.
Added new void-safe test project.
Minor Refactoring.

---

Revision 96822 - Directory Listing
Modified Thu Mar 12 15:42:28 2015 UTC (4 years, 9 months ago) by maxpei

Fixed a bug in the AutoDebug UI. Now the {Failing tests} column shows the total number of failing tests of the features.

---

Revision 96795 - Directory Listing
Modified Sun Mar 8 11:16:49 2015 UTC (4 years, 9 months ago) by schmisam

Added fix for mergeable conditionals
Removed fix for export can be restricted
Added tests for exoprt can be restricted

---

Revision 96783 - Directory Listing
Modified Fri Mar 6 13:07:59 2015 UTC (4 years, 9 months ago) by maxpei

Fixed a few bugs in AutoFix.
Added a command line argument to support experimental behavior.

---

Revision 96774 - Directory Listing
Modified Thu Mar 5 17:10:34 2015 UTC (4 years, 9 months ago) by maxpei

Fixed a problem during the termination of AutoFix due to time limit.

---

Revision 96671 - Directory Listing
Modified Fri Feb 27 05:01:22 2015 UTC (4 years, 9 months ago) by evemerge

<<Merged from trunk#96670.>>

---

Revision 96670 - Directory Listing
Modified Wed Feb 25 09:38:31 2015 UTC (4 years, 9 months ago) by maxpei

Fixed the mismatches across SOCKET read/write API usages, which caused "Retrieval error"s at runtime.

---

Revision 96662 - Directory Listing
Modified Fri Feb 20 05:19:57 2015 UTC (4 years, 9 months ago) by evemerge

<<Merged from trunk#96661.>>

---

Revision 96655 - Directory Listing
Modified Thu Feb 19 09:45:22 2015 UTC (4 years, 9 months ago) by manus

Merged from trunk rev#96592:
Added -D_ALLOW_MSC_VER_MISMATCH so that the code compiles with any versions of the Microsoft C++ compiler. This should be safe since we do not use any C++ standard libraries.

---

Revision 96615 - Directory Listing
Modified Fri Feb 13 05:16:08 2015 UTC (4 years, 9 months ago) by evemerge

<<Merged from trunk#96614.>>

---

Revision 96593 - Directory Listing
Modified Sat Feb 7 05:58:45 2015 UTC (4 years, 10 months ago) by schmisam

Improved performance of rule #73
Fixed a bug in rule #7
Changed fix for rule #5 to not use pretty printers anymore
Removed pretty printers from the code_analysis library
Refactored rule #75: New name

---

Revision 96591 - Directory Listing
Modified Fri Feb 6 03:21:12 2015 UTC (4 years, 10 months ago) by schmisam

Renamed file for rule #67's fix

---

Revision 96590 - Directory Listing
Modified Fri Feb 6 03:17:20 2015 UTC (4 years, 10 months ago) by schmisam

Changed implementation of rule #67
Updated test case for rule #67
Updated messages for rule #67

---

Revision 96588 - Directory Listing
Modified Thu Feb 5 13:16:37 2015 UTC (4 years, 10 months ago) by julian

improved error handling.

---

Revision 96587 - Directory Listing
Modified Thu Feb 5 11:47:45 2015 UTC (4 years, 10 months ago) by schmisam

Minor fix in rule #67

---

Revision 96586 - Directory Listing
Modified Thu Feb 5 11:41:26 2015 UTC (4 years, 10 months ago) by schmisam

Added exact copy of class FIX_UNUSED_LOCAL_APPLICATION to code_analysis library in order to make it available for use.

Added rule #87.
Added testcase for rule #87.

Fixed nested case in rule #50.
Adjusted testcase for rule #50.
Added fix for rule #50.

Changed implementation of fixes to use the new "execute" method for the general "move instruction within loop"-fix and the fixes for rules #47, #22, #37, #45, #16, #38, #15, #49 and #48.

Some code formatting of rules.

---

Revision 96581 - Directory Listing
Modified Wed Feb 4 14:15:36 2015 UTC (4 years, 10 months ago) by julian

disable debug output of AutoProof.
improved error messages.
fixed crashes on invalid decreases clause.

---

Revision 96580 - Directory Listing
Modified Wed Feb 4 13:29:57 2015 UTC (4 years, 10 months ago) by evemerge

<<Merged from trunk#96577.>>

---

Revision 96573 - Directory Listing
Modified Tue Feb 3 12:22:12 2015 UTC (4 years, 10 months ago) by julian

fixed EVE launch scripts.

---

Revision 96567 - Directory Listing
Modified Mon Feb 2 14:22:12 2015 UTC (4 years, 10 months ago) by manus

Integrated fix for displaying .NET classes in cluster tree. See rev#96566.

---

Revision 96530 - Directory Listing
Modified Fri Jan 23 20:29:28 2015 UTC (4 years, 10 months ago) by manus

Merged various changes from rev#96529:
- Fixed issues with IRON
- Support site bug fixes
- Minor cosmetics/warnings

---

Revision 96508 - Directory Listing
Modified Tue Jan 20 19:46:59 2015 UTC (4 years, 10 months ago) by manus

Merged changed from rev#96507.

---

Revision 96505 - Directory Listing
Modified Tue Jan 20 11:36:12 2015 UTC (4 years, 10 months ago) by manus

Merged from rev#96504.

---

Revision 96500 - Directory Listing
Modified Tue Jan 20 11:17:46 2015 UTC (4 years, 10 months ago) by manus

Used branch to perform the 15.01 release.

---

Revision 96499 - Directory Listing
Modified Tue Jan 20 11:13:32 2015 UTC (4 years, 10 months ago) by manus

Merged some version mismatch and early issues found in 15.01 from trunk at rev#96498.

---

Revision 96496 - Directory Listing
Modified Tue Jan 20 10:59:35 2015 UTC (4 years, 10 months ago) by manus

Fixed typo in path.

---

Revision 96487 - Directory Listing
Modified Tue Jan 20 08:28:43 2015 UTC (4 years, 10 months ago) by manus

Started the EiffelStudio 15.01 release

---

Revision 96424 - Directory Listing
Modified Tue Dec 23 21:37:12 2014 UTC (4 years, 11 months ago) by polikarn

Unified is_equal.

---

Revision 96423 - Directory Listing
Modified Tue Dec 23 00:55:09 2014 UTC (4 years, 11 months ago) by polikarn

Added independent is_equal implementatiion for hash table and set iterators.

---

Revision 96422 - Directory Listing
Modified Mon Dec 22 22:37:07 2014 UTC (4 years, 11 months ago) by polikarn

Added independent implementations of is_equal to HASH_TABLE and HASH_SET.

---

Revision 96419 - Directory Listing
Modified Mon Dec 22 21:59:01 2014 UTC (4 years, 11 months ago) by polikarn

BUGFIX: missing safety check conditions inside quantifiers. Fixed relations test.

---

Revision 96257 - Directory Listing
Modified Fri Dec 5 15:26:38 2014 UTC (5 years ago) by julian

Added ownership defaults for inlined routines.

---

Revision 96241 - Directory Listing
Modified Thu Dec 4 16:39:11 2014 UTC (5 years ago) by polikarn

Redesigned locking.

---

Revision 96187 - Directory Listing
Modified Fri Nov 28 14:33:08 2014 UTC (5 years ago) by schmisam

Bugfix

---

Revision 96182 - Directory Listing
Modified Fri Nov 28 08:51:18 2014 UTC (5 years ago) by schmisam

Changed fix for rule 50, using FIX_UNUSED_LOCAL_APPLICATION now.

---

Revision 96147 - Directory Listing
Modified Sun Nov 23 21:14:32 2014 UTC (5 years ago) by schmisam

Bugfixes for Undo Button for rule-fixing of code analyzer.
Added fixes for rules 50 and 07.
Added basic classes for rules 75 and 77 (WIP).
Added basic classes for fixes for rules 75 and 77 (WIP).
Adjusted test cases for rules 50 and 07.

---

Revision 96121 - Directory Listing
Modified Wed Nov 19 16:38:24 2014 UTC (5 years ago) by polikarn

Small fix.

---

Revision 96120 - Directory Listing
Modified Wed Nov 19 16:03:38 2014 UTC (5 years ago) by polikarn

Changed handling of inv gueard to improve performance in HASH_TABLE.

---

Revision 96106 - Directory Listing
Modified Mon Nov 17 17:57:30 2014 UTC (5 years ago) by polikarn

Bugfix in function encoding. Fixed tests. Added static annotations to EB2.

---

Revision 96103 - Directory Listing
Modified Mon Nov 17 16:30:08 2014 UTC (5 years ago) by polikarn

New translation for recursive functions. Fixed model replacement processing and removed the unsound frame redefinition. Bugfix: avoid crush when listing unknown attribute at model. Renamed dynamic status into nonvariant.

---

Revision 96100 - Directory Listing
Modified Mon Nov 17 12:32:08 2014 UTC (5 years ago) by julian

On Linux use Mono to launch Boogie.

---

Revision 96084 - Directory Listing
Modified Thu Nov 13 13:35:58 2014 UTC (5 years ago) by schmisam

Implemented Undo Fix button for code analysis tool panel.

---

Revision 96078 - Directory Listing
Modified Wed Nov 12 04:16:34 2014 UTC (5 years ago) by schmisam

Fixed bug in rule #48.
Changed tag "ca_ignoredby" to simply "ca_ignore".
Added tag "ca_only" to only check the given rule IDs (This will override any rules in tag "ca_ignore").

---

Revision 96077 - Directory Listing
Modified Tue Nov 11 22:02:31 2014 UTC (5 years ago) by julian

added flag to disable dynamic annotations.

---

Revision 96076 - Directory Listing
Modified Tue Nov 11 19:36:06 2014 UTC (5 years ago) by polikarn

Minor bugfix.

---

Revision 96074 - Directory Listing
Modified Mon Nov 10 18:12:23 2014 UTC (5 years, 1 month ago) by polikarn

Fixed incomplete specs in LIST.remove and remove_all.

---

Revision 96073 - Directory Listing
Modified Mon Nov 10 16:06:44 2014 UTC (5 years, 1 month ago) by polikarn

Removed redundant note.

---

Revision 96070 - Directory Listing
Modified Mon Nov 10 08:55:45 2014 UTC (5 years, 1 month ago) by schmisam

Integration of EiffelInspector into the Verification Assistant.

---

Revision 96053 - Directory Listing
Modified Fri Nov 7 15:17:37 2014 UTC (5 years, 1 month ago) by polikarn

Made more features dynamic.

---

Revision 96047 - Directory Listing
Modified Fri Nov 7 12:01:28 2014 UTC (5 years, 1 month ago) by polikarn

Added an option to disable independent inv check. Added another generic to LOCK.

---

Revision 96046 - Directory Listing
Modified Fri Nov 7 10:38:42 2014 UTC (5 years, 1 month ago) by julian

Initialize min_sleep_time for TTY rota task system.

---

Revision 96039 - Directory Listing
Modified Thu Nov 6 17:19:32 2014 UTC (5 years, 1 month ago) by polikarn

No default wrapping for dynamic methods. Put back opaque defs in hash table/iterator. Adapted some specs for the token counter.

---

Revision 96038 - Directory Listing
Modified Thu Nov 6 15:11:03 2014 UTC (5 years, 1 month ago) by julian

fixed window refresh after fix execution.

---

Revision 96037 - Directory Listing
Modified Thu Nov 6 13:38:09 2014 UTC (5 years, 1 month ago) by julian

aadded command line option to set maximum number of parallel Boogie instances.

---

Revision 96035 - Directory Listing
Modified Wed Nov 5 02:22:58 2014 UTC (5 years, 1 month ago) by schmisam

First steps in the integration of code analysis into the Verification Assistant.
Changed the folder structur in the blackboard wrappers to separate the different tools.

---

Revision 96032 - Directory Listing
Modified Tue Nov 4 12:19:41 2014 UTC (5 years, 1 month ago) by mschill

More features for net2

---

Revision 96029 - Directory Listing
Modified Sat Nov 1 15:22:18 2014 UTC (5 years, 1 month ago) by polikarn

Removed built-in attributes apart from subject and observers from the model. Static heurictic now works for all ghost fields.

---

Revision 96026 - Directory Listing
Modified Fri Oct 31 16:01:14 2014 UTC (5 years, 1 month ago) by julian

Fixed display of feature name in some results.
Added partial support for strings.

---

Revision 96017 - Directory Listing
Modified Thu Oct 30 11:55:25 2014 UTC (5 years, 1 month ago) by polikarn

Minor changes.

---

Revision 96010 - Directory Listing
Modified Tue Oct 28 16:47:56 2014 UTC (5 years, 1 month ago) by polikarn

Spec simplifications.

---

Revision 96008 - Directory Listing
Modified Tue Oct 28 12:06:25 2014 UTC (5 years, 1 month ago) by polikarn

Minor fixes and simplifications.

---

Revision 96001 - Directory Listing
Modified Mon Oct 27 13:13:27 2014 UTC (5 years, 1 month ago) by polikarn

Minor change in RANDOM.

---

Revision 95995 - Directory Listing
Modified Sun Oct 26 17:35:49 2014 UTC (5 years, 1 month ago) by polikarn

Added a test for a hash table client.

---

Revision 95994 - Directory Listing
Modified Sun Oct 26 16:58:21 2014 UTC (5 years, 1 month ago) by polikarn

Added RANDOM and some required integer functions.

---

Revision 95993 - Directory Listing
Modified Sun Oct 26 14:44:34 2014 UTC (5 years, 1 month ago) by polikarn

Minor changes.

---

Revision 95992 - Directory Listing
Modified Sun Oct 26 14:21:30 2014 UTC (5 years, 1 month ago) by polikarn

Fixed add_set/add_table in hash lock.

---

Revision 95991 - Directory Listing
Modified Sun Oct 26 13:16:10 2014 UTC (5 years, 1 month ago) by polikarn

Reimplemented hash set using has table.

---

Revision 95990 - Directory Listing
Modified Fri Oct 24 15:56:03 2014 UTC (5 years, 1 month ago) by polikarn

Rearranged the inheritance hierarchy (MAP is now the ancestor of TABLE but not of SEQUENCE).

---

Revision 95987 - Directory Listing
Modified Fri Oct 24 14:36:01 2014 UTC (5 years, 1 month ago) by polikarn

Added forget_iterator to hash table. Workaround a typing bug. Sound argument type in forget_iterator. Not verifying creation procedures with explicit contracts twice.

---

Revision 95985 - Directory Listing
Modified Fri Oct 24 09:01:18 2014 UTC (5 years, 1 month ago) by polikarn

Added copy_ to hash table.

---

Revision 95983 - Directory Listing
Modified Thu Oct 23 20:09:47 2014 UTC (5 years, 1 month ago) by polikarn

Added hash table resizing.

---

Revision 95982 - Directory Listing
Modified Thu Oct 23 16:05:56 2014 UTC (5 years, 1 month ago) by polikarn

Added most of HASH_TABLE and iterator. Added MML_PAIR. Functionals now produce axioms both from body and from post. Minor bug fixes.

---

Revision 95978 - Directory Listing
Modified Thu Oct 23 01:04:29 2014 UTC (5 years, 1 month ago) by schmisam

Added GUI stuff for code analysis tool panel.

---

Revision 95975 - Directory Listing
Modified Tue Oct 21 17:20:13 2014 UTC (5 years, 1 month ago) by polikarn

Added TABLE and iterator.

---

Revision 95974 - Directory Listing
Modified Tue Oct 21 14:42:31 2014 UTC (5 years, 1 month ago) by polikarn

Non-ghost code in HASH_SET using is_equal_ (as opposed to is_model_equal).

---

Revision 95972 - Directory Listing
Modified Tue Oct 21 13:28:34 2014 UTC (5 years, 1 month ago) by polikarn

Removed closed subjects requirement form is_equal.

---

Revision 95960 - Directory Listing
Modified Tue Oct 21 08:51:17 2014 UTC (5 years, 1 month ago) by polikarn

Included lock into set's subjects (simplified client contracts).

---

Revision 95956 - Directory Listing
Modified Mon Oct 20 15:29:34 2014 UTC (5 years, 1 month ago) by polikarn

Moved fresh_iterator functionality into interator.make. Added copy_ to hash_set_iterator.

---

Revision 95955 - Directory Listing
Modified Mon Oct 20 15:27:40 2014 UTC (5 years, 1 month ago) by julian

fixed test.

---

Revision 95954 - Directory Listing
Modified Mon Oct 20 11:44:59 2014 UTC (5 years, 1 month ago) by polikarn

Added copy_ to hash set, and stack and queue iterators. Simplified set.

---

Revision 95950 - Directory Listing
Modified Mon Oct 20 06:55:11 2014 UTC (5 years, 1 month ago) by julian

Added translation for more functions of reals.

---

Revision 95949 - Directory Listing
Modified Sun Oct 19 19:48:55 2014 UTC (5 years, 1 month ago) by polikarn

Added resizing to HASH_SET.

---

Revision 95948 - Directory Listing
Modified Sat Oct 18 14:51:23 2014 UTC (5 years, 1 month ago) by polikarn

Minor cleanup in HASH_SET and iterator.

---

Revision 95945 - Directory Listing
Modified Fri Oct 17 18:35:01 2014 UTC (5 years, 1 month ago) by polikarn

Bugfix in old_ handling.

---

Revision 95944 - Directory Listing
Modified Fri Oct 17 17:34:08 2014 UTC (5 years, 1 month ago) by polikarn

Fixed handling of old_. Finished HASH_SET and HASH_SET_ITERATOR (except resizing).

---

Revision 95938 - Directory Listing
Modified Fri Oct 17 04:58:59 2014 UTC (5 years, 1 month ago) by jasonw

<<Merged from trunk#95937.>>

---

Revision 95937 - Directory Listing
Modified Thu Oct 16 15:13:37 2014 UTC (5 years, 1 month ago) by julian

added translation of type adaptation.

---

Revision 95930 - Directory Listing
Modified Wed Oct 15 16:44:04 2014 UTC (5 years, 1 month ago) by polikarn

The bulk of HASH_SET and its iterator (except remove, add_iterator, forget_iterator, copy). Bugfix for logical targets.

---

Revision 95929 - Directory Listing
Modified Wed Oct 15 11:39:14 2014 UTC (5 years, 1 month ago) by julian

added more features to simple list and simple array.

---

Revision 95916 - Directory Listing
Modified Mon Oct 13 20:52:03 2014 UTC (5 years, 1 month ago) by julian

added across handlers for simple array and list.

---

Revision 95911 - Directory Listing
Modified Mon Oct 13 14:48:18 2014 UTC (5 years, 1 month ago) by maxpei

Changed the default setting of AutoFix tool; 
Fixed a bug in AutoFix which leads to more specification fixes than the maximum amount as given in the argument.

---

Revision 95910 - Directory Listing
Modified Mon Oct 13 11:40:10 2014 UTC (5 years, 1 month ago) by julian

fixed error message. added command-line options.

---

Revision 95908 - Directory Listing
Modified Sun Oct 12 19:26:31 2014 UTC (5 years, 1 month ago) by julian

refactoring of forked and bulk verification.

---

Revision 95907 - Directory Listing
Modified Sun Oct 12 14:05:53 2014 UTC (5 years, 1 month ago) by julian

Added new tests. Updated agents theory.

---

Revision 95893 - Directory Listing
Modified Fri Oct 10 09:23:16 2014 UTC (5 years, 2 months ago) by jasonw

<<Merged from trunk#95889.>>

---

Revision 95874 - Directory Listing
Modified Thu Oct 9 01:00:03 2014 UTC (5 years, 2 months ago) by schmisam

Added Fix me "button" (more like field for now...).
Segmentation fault in ES_CODE_ANALYSIS_TOOL (fix_column), workaround in place for now.

---

Revision 95873 - Directory Listing
Modified Wed Oct 8 21:14:28 2014 UTC (5 years, 2 months ago) by polikarn

Dynamic translation of guards. Bug fix in model definition generation.

---

Revision 95866 - Directory Listing
Modified Wed Oct 8 06:14:29 2014 UTC (5 years, 2 months ago) by julian

added command-line flag for forked- and bulk-verification.

---

Revision 95865 - Directory Listing
Modified Tue Oct 7 21:20:19 2014 UTC (5 years, 2 months ago) by polikarn

First version of HASH_SET.

---

Revision 95861 - Directory Listing
Modified Tue Oct 7 13:26:52 2014 UTC (5 years, 2 months ago) by polikarn

Added V_SET. Added default guard inv. Removed special guards from HASH_SET example.

---

Revision 95855 - Directory Listing
Modified Tue Oct 7 03:40:41 2014 UTC (5 years, 2 months ago) by schmisam

Added rules 50 and 87.
Added fix for rule 50.
Changed implementation of execution of fixes to increase performance in certain cases.
Added testcases for new rules.

---

Revision 95852 - Directory Listing
Modified Sun Oct 5 19:54:01 2014 UTC (5 years, 2 months ago) by julian

EVE: Fixed crash during precompilation.

---

Revision 95849 - Directory Listing
Modified Fri Oct 3 19:43:22 2014 UTC (5 years, 2 months ago) by julian

AutoProof: extracted note checks into helper class.

---

Revision 95848 - Directory Listing
Modified Fri Oct 3 13:37:39 2014 UTC (5 years, 2 months ago) by romanschmocker

Added scoop_patterns library to EVE branch.

---

Revision 95847 - Directory Listing
Modified Fri Oct 3 13:30:38 2014 UTC (5 years, 2 months ago) by romanschmocker

Initial test commit.

---

Revision 95842 - Directory Listing
Modified Thu Oct 2 19:56:14 2014 UTC (5 years, 2 months ago) by julian

AutoProof: fixed test output files.

---

Revision 95841 - Directory Listing
Modified Thu Oct 2 16:13:52 2014 UTC (5 years, 2 months ago) by polikarn

Fixed unsoundness (forgotten safety checks in the body of a functional). Taking semistrict operators into account also in the body expression translator.

---

Revision 95840 - Directory Listing
Modified Thu Oct 2 15:09:05 2014 UTC (5 years, 2 months ago) by julian

AutoProof: cleaned up options, refactored feature and class status notes.

---

Revision 95839 - Directory Listing
Modified Thu Oct 2 14:16:16 2014 UTC (5 years, 2 months ago) by polikarn

Finished set example. Added setter routines. Added deafult_create postcondition. Termination checks are currently broken for functionals.

---

Revision 95836 - Directory Listing
Modified Thu Oct 2 05:30:48 2014 UTC (5 years, 2 months ago) by schmisam

Added fix for rule #45.
Some refactoring.

---

Revision 95835 - Directory Listing
Modified Thu Oct 2 05:01:30 2014 UTC (5 years, 2 months ago) by schmisam

Added rule #45 and tests for it.

---

Revision 95834 - Directory Listing
Modified Thu Oct 2 03:48:07 2014 UTC (5 years, 2 months ago) by schmisam

Last commit didn't compile. Fixed.

---

Revision 95833 - Directory Listing
Modified Thu Oct 2 03:27:05 2014 UTC (5 years, 2 months ago) by schmisam

Trying to fix svn:ignore property on Src/framework/code_analysis/tests

---

Revision 95832 - Directory Listing
Modified Wed Oct 1 21:50:22 2014 UTC (5 years, 2 months ago) by schmisam

Reverted base2 dependency on code_analysis/tests
Added tests.ecf file to ignored files (in case somebody wants to add other libraries for testing without commiting)

---

Revision 95830 - Directory Listing
Modified Wed Oct 1 18:42:26 2014 UTC (5 years, 2 months ago) by schmisam

Added rules 7 and 9.
Added tests for rules.

---

Revision 95829 - Directory Listing
Modified Tue Sep 30 16:47:44 2014 UTC (5 years, 2 months ago) by polikarn

Hash set example with a lock. Minor bugfixes.

---

Revision 95828 - Directory Listing
Modified Tue Sep 30 15:31:08 2014 UTC (5 years, 2 months ago) by schmisam

Debugging of rules.
Changed the way inline agent objects in the AST are processed during code-analysis to prevent exceptions.

---

Revision 95822 - Directory Listing
Modified Mon Sep 29 15:58:08 2014 UTC (5 years, 2 months ago) by polikarn

Bugfix (invariant caching).

---

Revision 95821 - Directory Listing
Modified Mon Sep 29 12:37:42 2014 UTC (5 years, 2 months ago) by polikarn

Adapted contracts of SIMPLE_LIST and SIMPLE_ARRAY to new defaults.

---

Revision 95820 - Directory Listing
Modified Mon Sep 29 08:41:38 2014 UTC (5 years, 2 months ago) by julian

AutoProof: fixed bug in termination check.

---

Revision 95814 - Directory Listing
Modified Sun Sep 28 16:20:52 2014 UTC (5 years, 2 months ago) by polikarn

Added a simple hash set to tests (no sharing as yet).

---

Revision 95813 - Directory Listing
Modified Sun Sep 28 13:33:17 2014 UTC (5 years, 2 months ago) by polikarn

Added back some base theory axioms (Void type, boxing). Translating actual generic parameters. Translating once functions as constants. Excluded fields closed, owner from read frames.

---

Revision 95810 - Directory Listing
Modified Fri Sep 26 04:48:53 2014 UTC (5 years, 2 months ago) by jasonw

<<Merged from trunk#95809.>>

---

Revision 95804 - Directory Listing
Modified Thu Sep 25 12:31:28 2014 UTC (5 years, 2 months ago) by polikarn

Replaced is_equal with is_equal_ because of like Current types. Fixed some bugs in type_property.

---

Revision 95803 - Directory Listing
Modified Wed Sep 24 16:04:19 2014 UTC (5 years, 2 months ago) by julian

AutoProof: added contract tags for simple array.

---

Revision 95794 - Directory Listing
Modified Tue Sep 23 15:59:15 2014 UTC (5 years, 2 months ago) by julian

AutoProof: adding SIMPLE_LIST equivalent to SIMPLE_ARRAY.

---

Revision 95788 - Directory Listing
Modified Mon Sep 22 20:51:59 2014 UTC (5 years, 2 months ago) by apaolo

Small final tweaks. Most notably:
-New queries `{AT_BLOCK_TYPE}.is_complex' and `is_atomic'. Replaced all uses of `{AT_ENUM_BLOCK_TYPE}.is_complex_block_type' with this.
-Deferred features now handled properly (the `deferred' keyword is considered to be the `routine_body'.
-Command line usage is now a bit more user friendly.

---

Revision 95787 - Directory Listing
Modified Mon Sep 22 15:45:45 2014 UTC (5 years, 2 months ago) by polikarn

New semantics of is_equal.

---

Revision 95777 - Directory Listing
Modified Mon Sep 22 09:24:19 2014 UTC (5 years, 2 months ago) by polikarn

Changed default contracts for functions to require that the args be closed and to read universe (except functional).

---

Revision 95773 - Directory Listing
Modified Fri Sep 19 11:31:17 2014 UTC (5 years, 2 months ago) by polikarn

Added ARRAY2.

---

Revision 95772 - Directory Listing
Modified Fri Sep 19 07:01:09 2014 UTC (5 years, 2 months ago) by jasonw

<<Merged from trunk#95771.>>

---

Revision 95770 - Directory Listing
Modified Wed Sep 17 16:03:49 2014 UTC (5 years, 2 months ago) by polikarn

Improved adding iterators, unfroze implementations, fixed unpredictability in ARRAY.

---

Revision 95769 - Directory Listing
Modified Wed Sep 17 12:39:30 2014 UTC (5 years, 2 months ago) by polikarn

Added ARRAYED_LIST. Fixed unpredictability in reverse (ll and dll).

---

Revision 95765 - Directory Listing
Modified Tue Sep 16 16:17:09 2014 UTC (5 years, 2 months ago) by polikarn

Added verification times to comand-line output. Bugfix for empty reads clauses.

---

Revision 95762 - Directory Listing
Modified Sat Sep 13 16:04:21 2014 UTC (5 years, 2 months ago) by hagedoch

final commit by hagedoch

---

Revision 95761 - Directory Listing
Modified Sat Sep 13 16:03:00 2014 UTC (5 years, 2 months ago) by hagedoch

json_error_displayer.e by hagedoch

---

Revision 95760 - Directory Listing
Modified Sat Sep 13 16:01:28 2014 UTC (5 years, 2 months ago) by hagedoch

json_error_displayer.e by hagedoch

---

Revision 95759 - Directory Listing
Modified Sat Sep 13 16:00:29 2014 UTC (5 years, 2 months ago) by hagedoch

json_format.e by hagedoch

---

Revision 95758 - Directory Listing
Modified Fri Sep 12 12:26:12 2014 UTC (5 years, 2 months ago) by schmisam

Deletion of accidentally commited files.

---

Revision 95757 - Directory Listing
Modified Fri Sep 12 12:25:28 2014 UTC (5 years, 2 months ago) by schmisam

Added Unreachable Code rule and rule for invariant loop computation within loop
Reworked object_creation_within_loop_fix to work for several rules
Added tests for the new rules

---

Revision 95753 - Directory Listing
Modified Tue Sep 9 15:43:48 2014 UTC (5 years, 3 months ago) by polikarn

Added reads universe; static model query redefinitions take precedence.

---

Revision 95748 - Directory Listing
Modified Mon Sep 8 15:24:50 2014 UTC (5 years, 3 months ago) by polikarn

Taking the latest definition for static model queries. Excluding dynamic routines from non-bulk verification.

---

Revision 95747 - Directory Listing
Modified Mon Sep 8 14:27:54 2014 UTC (5 years, 3 months ago) by polikarn

Excluding observers from ownership defaults. Allow calling creators from creators. Added ARRAY and ARRAY_ITERATOR.

---

Revision 95746 - Directory Listing
Modified Fri Sep 5 16:24:19 2014 UTC (5 years, 3 months ago) by polikarn

Added INDEX_ITERATOR and a wrapper for SPECIAL.

---

Revision 95745 - Directory Listing
Modified Fri Sep 5 09:09:00 2014 UTC (5 years, 3 months ago) by polikarn

Added doubly-linked list; bugfix; minor spec simplifications.

---

Revision 95744 - Directory Listing
Modified Thu Sep 4 16:19:21 2014 UTC (5 years, 3 months ago) by apaolo

Moved the default two hint tables to text files. They are now also loaded from file using class AT_LOADABLE_HINT_TABLE.
The minimum hint level is now effectively zero when loading tables from file. Now level zero is to be considered the input given to students.
Bugfix in AT_LOADABLE_HINT_TABLE: loading a table with an invalid block name would have erroneously triggered the "block already present" error message.

---

Revision 95743 - Directory Listing
Modified Thu Sep 4 16:18:37 2014 UTC (5 years, 3 months ago) by apaolo

Fixed two unrelated internal bugs that were not affecting the output but were causing invariant violations when invariant checking was enabled.

---

Revision 95742 - Directory Listing
Modified Wed Sep 3 21:53:49 2014 UTC (5 years, 3 months ago) by apaolo

Change to how loop termination conditions and variants are handled. Now in both cases we have a complex block including the "until"/"variant" keyword and an atomic block inside it, with the boolean/integer expression. The handling was inconsistent until now, in the first case there was no complex block (so no way to hide the "until" keyword if you were showing the loop), in the second there was no atomic block, and you could only work on complex block loop_variant and its content visibility.

---

Revision 95741 - Directory Listing
Modified Wed Sep 3 21:53:05 2014 UTC (5 years, 3 months ago) by apaolo

Renamed AT_TRI_STATE_BOOLEAN to AT_TRILEAN.

---

Revision 95739 - Directory Listing
Modified Wed Sep 3 15:20:48 2014 UTC (5 years, 3 months ago) by apaolo

Several small changes originating from feedback from the code review:
-Removed the hint level limit. Any natural number is now a valid hint level.
-Created a proper conversion from AT_TRI_STATE_BOOLEAN (soon to be renamed to AT_TRILEAN or TRILEAN) to BOOLEAN.
-Language strings with parameters are now translated the right way.
-Change to class AT_AUTOTEACH. Feature `process_class' is now exposed, and does not write to a file directly. Instead, it stores the result in a new class field, which is also exposed. This makes it easier to access the result programmatically (which is not a necessity now, but it might be in the future).

---

Revision 95737 - Directory Listing
Modified Tue Sep 2 17:06:21 2014 UTC (5 years, 3 months ago) by polikarn

Implemented dynamic methods. Removed free preconditions of functions (not really needed). Bugfixes.

---

Revision 95731 - Directory Listing
Modified Tue Sep 2 11:12:17 2014 UTC (5 years, 3 months ago) by apaolo

Moved all initialization features to the beginning of the respective classes.
Deleted folder 'commands' as it only contained one class (AT_COMMAND). Moved AT_COMMAND outside.

---

Revision 95730 - Directory Listing
Modified Tue Sep 2 11:05:06 2014 UTC (5 years, 3 months ago) by apaolo

Made AT_ENUM a generic class, constrained to AT_ENUM_VALUE (AT_ENUM [G -> AT_ENUM_VALUE]). Should have done like this from the beginning.
Removed that ugly value_type feature.

---

Revision 95729 - Directory Listing
Modified Tue Sep 2 11:04:23 2014 UTC (5 years, 3 months ago) by apaolo

Minor changes and fixes for addressing issues found in the code review.
https://docs.google.com/document/d/1MLzZoY0xJGfmPGev259Dn4eKbb3_LsGGlVlPJ-JOkx0/edit?usp=sharing

---

Revision 95728 - Directory Listing
Modified Tue Sep 2 11:03:39 2014 UTC (5 years, 3 months ago) by apaolo

Everything in class AT_ENUM:
-refactoring, now using hash tables internally for faster lookup.
-removed features `values_names' and `numerical_values'.
-fixed bug: once ("PROCESS") instead of once ("OBJECT") in feature textual_value_list.

---

Revision 95724 - Directory Listing
Modified Mon Sep 1 14:19:48 2014 UTC (5 years, 3 months ago) by apaolo

Moved initialization to a separate feature clause in all classes where this was not the case.

---

Revision 95723 - Directory Listing
Modified Mon Sep 1 10:26:22 2014 UTC (5 years, 3 months ago) by polikarn

Added queues.

---

Revision 95722 - Directory Listing
Modified Mon Sep 1 10:20:06 2014 UTC (5 years, 3 months ago) by polikarn

Added LINKED_STACK_ITERATOR

---

Revision 95721 - Directory Listing
Modified Sun Aug 31 15:09:53 2014 UTC (5 years, 3 months ago) by polikarn

Fixed unsoundness in type properties. Removed unused invariant declarations. Simplified intervals.

---

Revision 95720 - Directory Listing
Modified Sat Aug 30 22:13:34 2014 UTC (5 years, 3 months ago) by apaolo

Fix: textual hints in hidden region were still printed with their original indentation instead of the "placeholder indentation" at their location in the output. There was code for doing it, but it was not working as expected.
Change: printing a textual hints now resets the `blank_line_inserted' and `placeholder_inserted' flags, resulting in a new placeholder being printed if more code is hidden after the hint.

---

Revision 95719 - Directory Listing
Modified Fri Aug 29 16:45:34 2014 UTC (5 years, 3 months ago) by polikarn

Fixed read frame checks.

---

Revision 95718 - Directory Listing
Modified Fri Aug 29 16:16:58 2014 UTC (5 years, 3 months ago) by polikarn

Improved verification results/speed.

---

Revision 95717 - Directory Listing
Modified Fri Aug 29 12:56:08 2014 UTC (5 years, 3 months ago) by julian

AutoProof: improvements to verification in isolation.

---

Revision 95716 - Directory Listing
Modified Fri Aug 29 07:48:23 2014 UTC (5 years, 3 months ago) by julian

AutoProof: added option to verify all routines of a class in isolation.

---

Revision 95713 - Directory Listing
Modified Fri Aug 29 04:56:42 2014 UTC (5 years, 3 months ago) by jasonw

<<Merged from trunk#95712.>>

---

Revision 95712 - Directory Listing
Modified Thu Aug 28 20:46:33 2014 UTC (5 years, 3 months ago) by apaolo

Added missing (forgotten) visibility entry for class_invariant in the default 'auto' table.
Also explicitly added undefined entries for all the missing atomic blocks.

---

Revision 95711 - Directory Listing
Modified Thu Aug 28 18:10:18 2014 UTC (5 years, 3 months ago) by polikarn

Verified all features in LINKED_LIST. Improved invariant violation reporting. Bugfixes.

---

Revision 95710 - Directory Listing
Modified Thu Aug 28 16:46:25 2014 UTC (5 years, 3 months ago) by apaolo

Support for open ranges of hint levels, e.g. "3-" means from 3 to infinity, "-7" means "up to level 7", "-" means from zero to infinity.
Hint levels are now represented with a NATURAL instead of an INTEGER.
Refactored class AT_HINT_TABLE to reduce code duplication.

---

Revision 95709 - Directory Listing
Modified Thu Aug 28 13:21:34 2014 UTC (5 years, 3 months ago) by apaolo

Fixed problem with blank lines and textual hints. I really can't believe how hard getting it right seems to be! I really hope this is the last time I have to touch this.
Fixed incorrect indentation of hints after if, loop and inspect blocks.
Fixed AutoTeach messages no longer being printed after a recent refactoring.

---

Revision 95706 - Directory Listing
Modified Wed Aug 27 15:30:17 2014 UTC (5 years, 3 months ago) by apaolo

Renamed everywhere "policy type" to "policy strength", it should be clearer.

---

Revision 95701 - Directory Listing
Modified Sat Aug 23 01:19:55 2014 UTC (5 years, 3 months ago) by schmisam

Added Fixes for rules: #48, #49, #15, #38, #16, #19 (included in #3), #68, #37, #47
Added code analysis rule #19 and #48
Added tests for rules #19 and #48
Cleaned up a lot of the older rules
Added Mac OSX 64bit specific files to svn ignore property on several folders

---

Revision 95699 - Directory Listing
Modified Fri Aug 22 04:53:38 2014 UTC (5 years, 3 months ago) by jasonw

<<Merged from trunk#95698.>>

---

Revision 95698 - Directory Listing
Modified Thu Aug 21 21:57:56 2014 UTC (5 years, 3 months ago) by apaolo

Some cleanup and tidying up.
One single instance of iterator is now used for a whole run of AutoTeach.
Treat feature comments as if they were a part of the feature declaration (always print them if the feature is visibile).

---

Revision 95697 - Directory Listing
Modified Thu Aug 21 15:20:57 2014 UTC (5 years, 3 months ago) by apaolo

Fixed very stupid mistake, of course if instruction may not have an else branch at all.

---

Revision 95696 - Directory Listing
Modified Thu Aug 21 15:20:29 2014 UTC (5 years, 3 months ago) by apaolo

Analyzed the whole project with Inspector Eiffel, fixed all the unintended violations.

---

Revision 95695 - Directory Listing
Modified Thu Aug 21 15:19:31 2014 UTC (5 years, 3 months ago) by apaolo

Fix: then, else, from and loop keywords were not being handled as a part of if_branch, if_branch, loop_initialization and loop_body respectively.

---

Revision 95694 - Directory Listing
Modified Thu Aug 21 15:19:00 2014 UTC (5 years, 3 months ago) by apaolo

Small but nasty fix of newline problems with textual hints.

---

Revision 95693 - Directory Listing
Modified Thu Aug 21 15:18:33 2014 UTC (5 years, 3 months ago) by apaolo

Support multiple block types on the same line for commands working on block types.

---

Revision 95692 - Directory Listing
Modified Thu Aug 21 15:18:01 2014 UTC (5 years, 3 months ago) by apaolo

Implemented multi-line hints (with a new special hint continuation command).
More verbose output in case of error when processing commands.
Reorganized several strings in AT_STRINGS.

---

Revision 95691 - Directory Listing
Modified Thu Aug 21 15:17:12 2014 UTC (5 years, 3 months ago) by apaolo

Support selecting mode from the command line. Changed syntax for mode-switching meta-commands.

---

Revision 95690 - Directory Listing
Modified Thu Aug 21 15:16:22 2014 UTC (5 years, 3 months ago) by apaolo

Renamed "unannotated mode" to "auto mode" and "hint mode" to "manual mode". Created new enum type for modes.

---

Revision 95689 - Directory Listing
Modified Thu Aug 21 15:15:31 2014 UTC (5 years, 3 months ago) by apaolo

Fixed parsing levels of commands.

---

Revision 95688 - Directory Listing
Modified Thu Aug 21 15:15:02 2014 UTC (5 years, 3 months ago) by apaolo

Significant cleanup, commenting and refactoring of the oracle class.
Output files are now created lowercase. A message is printed at the beginning of the processing of every class.

---

Revision 95687 - Directory Listing
Modified Thu Aug 21 15:14:27 2014 UTC (5 years, 3 months ago) by apaolo

Refactored command parsing into an external class.

---

Revision 95686 - Directory Listing
Modified Thu Aug 21 15:13:56 2014 UTC (5 years, 3 months ago) by apaolo

Further modified the default unannotated visibility table so that, once a block becomes visible (True) at level n, its visibility from levels n+1 on is omitted and left as implicit. This should make easier to see what is actually changing at each level.
Also added one more level. Instructions outside any if/loop/inspect, which might be initialization or finalization instructions, are now shown at level 7, while the body of if/loop/inspect statements is still omitted.

---

Revision 95685 - Directory Listing
Modified Thu Aug 21 15:13:25 2014 UTC (5 years, 3 months ago) by apaolo

Rewritten default hint tables using T/F/U abbreviations for tri-state booleans for better readability.

---

Revision 95663 - Directory Listing
Modified Fri Aug 15 21:08:49 2014 UTC (5 years, 3 months ago) by apaolo

Made class names in arguments case-insensitive.

---

Revision 95662 - Directory Listing
Modified Fri Aug 15 16:52:01 2014 UTC (5 years, 3 months ago) by apaolo

Changes to how comments/breaks are handled regarding the content visibility.
Added meta-comments. These are comments regarding annotations which are ignored by AutoTeach and never appear in the output. It is practically implemented as a new metacommand where the keyword is '#', the syntax derives from this.
Colons after a metacommand keyword are now tolerated.
Parsing tri-state booleans now support more string representations.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 15/08/2014 16:45:32 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 15/08/2014 16:47:31 +02:00

---

Revision 95661 - Directory Listing
Modified Fri Aug 15 16:51:14 2014 UTC (5 years, 3 months ago) by apaolo

The visibility table in hint tables doesn't have to be complete anymore. Any missing entries will be considered to be undefined, as it was for the content visibility table already.
Fixed bug: oracle.begin_process_class and end_process_class not being called. I cannot believe I haven't noticed this before.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 15/08/2014 16:45:32 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 15/08/2014 16:47:31 +02:00

---

Revision 95660 - Directory Listing
Modified Fri Aug 15 16:50:34 2014 UTC (5 years, 3 months ago) by apaolo

New options: support for a range of hint levels (AutoTeach will be executed multiple times, once for every hint level), option to create a subfolder for each hint level and place the output there.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 15/08/2014 16:45:32 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 15/08/2014 16:47:31 +02:00

---

Revision 95659 - Directory Listing
Modified Fri Aug 15 16:49:42 2014 UTC (5 years, 3 months ago) by apaolo

Killed the "Hinter" brand. As no other modules and tools are planned, AutoTeach *IS* the old Hinter, no need for another name.
(and "Hinter" was really horrible, let's face it)
Rearranged files, replaced every occurrence of "hinter" in the whole project, removed the mandatory "-at-hinter" command line switch.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 15/08/2014 16:45:32 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 15/08/2014 16:47:31 +02:00

---

Revision 95658 - Directory Listing
Modified Fri Aug 15 08:58:51 2014 UTC (5 years, 3 months ago) by jasonw

<<Merged from trunk#95657.>>

---

Revision 95657 - Directory Listing
Modified Thu Aug 14 09:32:20 2014 UTC (5 years, 3 months ago) by apaolo

Added two missing classes, sorry for breaking the branch!

---

Revision 95656 - Directory Listing
Modified Wed Aug 13 15:08:27 2014 UTC (5 years, 3 months ago) by apaolo

Naming change: "simple blocks" become "atomic blocks". Replaced 'simple' with atomic in the whole project.
The main implementation should finally be complete!
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 15:06:24 +00:00

---

Revision 95655 - Directory Listing
Modified Wed Aug 13 15:07:44 2014 UTC (5 years, 3 months ago) by apaolo

Got rid of the concept of hybrid blocks. Instead, now any complex block can be treated as simple. Unlike with hybrid blocks, the block will retain its original type (an if will stay an if, it will not be turned into an instruction), but it will be treated as a simple block.
Fixed an oversight in the default unannotated hint table.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 15:06:24 +00:00

---

Revision 95654 - Directory Listing
Modified Wed Aug 13 15:07:03 2014 UTC (5 years, 3 months ago) by apaolo

Added support for obscuring single argument or local declarations, where with single declaration we mean a list of identifier and the type.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 15:06:24 +00:00

---

Revision 95653 - Directory Listing
Modified Wed Aug 13 15:05:35 2014 UTC (5 years, 3 months ago) by apaolo

Fixed generic arguments of named tuples being treated as if they were routine arguments.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 15:00:29 +00:00

---

Revision 95652 - Directory Listing
Modified Wed Aug 13 15:05:03 2014 UTC (5 years, 3 months ago) by apaolo

Several things. Most notably, made blocks visibility in hint tables a tri-state boolean too (like content visibilities).
Changed and made more consistent the order of priorities of annotations and visibilities. Created new class AT_ENUM_POLICY_TYPE helping with this.
Rewritten hint tables accordingly.
Some other minor changes.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 15:00:29 +00:00

---

Revision 95651 - Directory Listing
Modified Wed Aug 13 15:04:02 2014 UTC (5 years, 3 months ago) by apaolo

Completed the default unannotated hint table.
Made a small, yet relevant, change to how content visibility of nested complex blocks is treated.
Found a logical inconsistency: written a long comment to explain it so that it can be addressed in some way in the future.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 15:00:29 +00:00

---

Revision 95650 - Directory Listing
Modified Wed Aug 13 15:03:29 2014 UTC (5 years, 3 months ago) by apaolo

Small fix related to outputting hints and indentation.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 15:00:29 +00:00

---

Revision 95649 - Directory Listing
Modified Wed Aug 13 15:02:59 2014 UTC (5 years, 3 months ago) by apaolo

Fixed loading the custom hint table from file. It seems that once routines and non-conforming inheritance don't really mix well. Now it should really work.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 15:00:29 +00:00

---

Revision 95648 - Directory Listing
Modified Wed Aug 13 15:02:04 2014 UTC (5 years, 3 months ago) by apaolo

Implemented actual loading of the custom hint table from file.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 15:00:29 +00:00

---

Revision 95647 - Directory Listing
Modified Wed Aug 13 15:01:08 2014 UTC (5 years, 3 months ago) by apaolo

Support for 'inspect' blocks.
The implementation of the main processing engine is finally complete!!!
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 15:00:29 +00:00

---

Revision 95646 - Directory Listing
Modified Wed Aug 13 14:54:20 2014 UTC (5 years, 3 months ago) by apaolo

Full support for loops. Seems to be working perfectly!
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95645 - Directory Listing
Modified Wed Aug 13 14:53:37 2014 UTC (5 years, 3 months ago) by apaolo

Converted arguments from complex to simple block. Parentheses are considered to be a part of the routine declaration.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95644 - Directory Listing
Modified Wed Aug 13 14:53:03 2014 UTC (5 years, 3 months ago) by apaolo

Changes to AT_ENUM_BLOCK_TYPE so that a contract is actually preventing uninitialized enum values from being read.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95643 - Directory Listing
Modified Wed Aug 13 14:52:22 2014 UTC (5 years, 3 months ago) by apaolo

Lots of cleanup. In particular, written feature comments for all the features in all classes where it was missing.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95642 - Directory Listing
Modified Wed Aug 13 14:51:19 2014 UTC (5 years, 3 months ago) by apaolo

Reorganized feature clauses in AT_HINTER_PROCESSING_ORACLE.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95641 - Directory Listing
Modified Wed Aug 13 14:50:42 2014 UTC (5 years, 3 months ago) by apaolo

Removed some now redundant code in the iterator class.
Renamed 'defined' to 'is_defined' in class 'AT_TRI_STATE_BOOLEAN'.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95640 - Directory Listing
Modified Wed Aug 13 14:50:04 2014 UTC (5 years, 3 months ago) by apaolo

Support for hybrid blocks.
Hybrid blocks are complex blocks that can also be treated as simple blocks. Every type of hybrid block has a corresponding simple block. Currently the only hybrid block is 'if', and its corresponding simple block is 'instruction', meaning that if instructions can now optionally be processed as if they were a single instruction (which translates to all or nothing). If an 'if' statement is processed as a simple instruction, it is really handled as if it were a simple instruction. This means that, for example, if a "#SHOW_NEXT if" command is pending, the command will *not* be applied to the subsequent if-as-simple-instruction block, because that block is effectively a simple instruction.
The implementation of this is probably not the simplest possible, but it is made so that all the complexity is within the oracle. The iterator class doesn't have to care and must just blindly trust the oracle.
Created new TREAT_[NEXT|ALL]_AS_[SIMPLE|COMPLEX] commands.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95639 - Directory Listing
Modified Wed Aug 13 14:49:17 2014 UTC (5 years, 3 months ago) by apaolo

Made all bt_ and ph_ constants uppercase.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95638 - Directory Listing
Modified Wed Aug 13 14:48:27 2014 UTC (5 years, 3 months ago) by apaolo

Support for inline hiding of if conditions. Everything seems to be working great. Some related refactoring.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95637 - Directory Listing
Modified Wed Aug 13 14:47:46 2014 UTC (5 years, 3 months ago) by apaolo

Support for if instructions. Everything seems to work perfectly, except that the if conditions are not obscured inline (yet).
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95636 - Directory Listing
Modified Wed Aug 13 14:47:02 2014 UTC (5 years, 3 months ago) by apaolo

Added two missing classes. (unversioned, lost with git cleanup and rewritten from scratch...)
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95635 - Directory Listing
Modified Wed Aug 13 14:46:21 2014 UTC (5 years, 3 months ago) by apaolo

Outputting hints works like a charm!
Cleared some TODOs.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95634 - Directory Listing
Modified Wed Aug 13 14:45:18 2014 UTC (5 years, 3 months ago) by apaolo

Cleaned up large sections of commented code. Prettified all classes.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95633 - Directory Listing
Modified Wed Aug 13 14:44:15 2014 UTC (5 years, 3 months ago) by apaolo

Hiding features and locals seems to be working as well. *MASSIVE* code cleanup is coming!
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95632 - Directory Listing
Modified Wed Aug 13 14:43:36 2014 UTC (5 years, 3 months ago) by apaolo

Everything works like a charm for now.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95631 - Directory Listing
Modified Wed Aug 13 14:43:00 2014 UTC (5 years, 3 months ago) by apaolo

Undoing changes to ecf file, committed by mistake for the second time.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95630 - Directory Listing
Modified Wed Aug 13 14:42:33 2014 UTC (5 years, 3 months ago) by apaolo

Processing routine bodies and instructions seems to work fine. Annotations seem to work fine too.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95629 - Directory Listing
Modified Wed Aug 13 14:41:49 2014 UTC (5 years, 3 months ago) by apaolo

Insert special placeholder for arguments. Created new enum for placeholders.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95628 - Directory Listing
Modified Wed Aug 13 14:40:54 2014 UTC (5 years, 3 months ago) by apaolo

Cleanup: renamed AT_HINTER_BLOCK_VISIBILITY to AT_BLOCK_VISIBILITY, mad 'tri_' constants uppercase.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95627 - Directory Listing
Modified Wed Aug 13 14:40:04 2014 UTC (5 years, 3 months ago) by apaolo

After the long refactoring, the code finally seems to work, at least as a proof-of-concept with class invariants. A small change to class AST_ROUNDTRIP_PRINTER_VISITOR was unfortunately unavoidable.
A lot of cleanup is coming soon.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95626 - Directory Listing
Modified Wed Aug 13 14:39:09 2014 UTC (5 years, 3 months ago) by apaolo

Work in progress. At least it seems to run without segmentation faults, after several clean-compilations...
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 13/08/2014 14:36:44 +02:00

---

Revision 95625 - Directory Listing
Modified Wed Aug 13 14:28:05 2014 UTC (5 years, 3 months ago) by apaolo

Done with most of the changes in the oracle class. Must still update the iterator class, still doesn't compile.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95624 - Directory Listing
Modified Wed Aug 13 14:27:15 2014 UTC (5 years, 3 months ago) by apaolo

Intermediate commit. NOT COMPILING!
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95623 - Directory Listing
Modified Wed Aug 13 14:26:21 2014 UTC (5 years, 3 months ago) by apaolo

Done tampering with enums, hopefully!
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95622 - Directory Listing
Modified Wed Aug 13 14:21:26 2014 UTC (5 years, 3 months ago) by apaolo

One more work-in-progress commit.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95621 - Directory Listing
Modified Wed Aug 13 14:20:18 2014 UTC (5 years, 3 months ago) by apaolo

Huge work-in-progress commit. Added enum classes.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95620 - Directory Listing
Modified Wed Aug 13 14:19:20 2014 UTC (5 years, 3 months ago) by apaolo

Work in progress: created new AT_HINTER_BLOCK_VISIBILITY class and a visibility table, added some TODOs
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95619 - Directory Listing
Modified Wed Aug 13 14:18:40 2014 UTC (5 years, 3 months ago) by apaolo

Now there should be no problems anymore if a command keyword happens to be a prefix of another one.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95618 - Directory Listing
Modified Wed Aug 13 14:16:31 2014 UTC (5 years, 3 months ago) by apaolo

Ignore commands in a skipped routine.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95617 - Directory Listing
Modified Wed Aug 13 14:15:56 2014 UTC (5 years, 3 months ago) by apaolo

Reverting an accidentally committed change to ec.ecf.

Conflicts:
	Eiffel/Ace/ec.ecf
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95616 - Directory Listing
Modified Wed Aug 13 14:15:28 2014 UTC (5 years, 3 months ago) by apaolo

Added hint tables! Hint tables define whether a certain block type should be showed by default or not at a certain hint level.

Several other smaller changes. Changed to {NONE} the visibility of most members of AT_COMMON and similar classes, so that we don't clutter the "feature namespace", and switched to non-conforming inheritance.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95615 - Directory Listing
Modified Wed Aug 13 14:14:38 2014 UTC (5 years, 3 months ago) by apaolo

Changed the syntax of meta-commands. Now a level can be specified for all of them, not just hints.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95614 - Directory Listing
Modified Wed Aug 13 14:13:58 2014 UTC (5 years, 3 months ago) by apaolo

Support a new meta-command for enabling/disabling the code placeholder.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95613 - Directory Listing
Modified Wed Aug 13 14:13:21 2014 UTC (5 years, 3 months ago) by apaolo

Moved all the processing logic to the oracle class.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95612 - Directory Listing
Modified Wed Aug 13 14:12:51 2014 UTC (5 years, 3 months ago) by apaolo

Support skipping features entirely.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95611 - Directory Listing
Modified Wed Aug 13 14:12:12 2014 UTC (5 years, 3 months ago) by apaolo

Big commit.
Most notable changes:
-Removed class AT_HINTER_CLASS_PROCESSOR. Moved its only method to AT_HINTER.
-Created new class AT_HINTER_PROCESSING_ORACLE, which is going to be questioned every time we have to decide whether to hide or show some code region.
-Created new class: AT_TRI_STATE_BOOLEAN
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95610 - Directory Listing
Modified Wed Aug 13 14:11:30 2014 UTC (5 years, 3 months ago) by apaolo

More indentation fixes. ...
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95609 - Directory Listing
Modified Wed Aug 13 14:11:02 2014 UTC (5 years, 3 months ago) by apaolo

Supports obscuring routine arguments.

Conflicts:
	Eiffel/Ace/ec.ecf
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95608 - Directory Listing
Modified Wed Aug 13 14:10:20 2014 UTC (5 years, 3 months ago) by apaolo

Hide local variables.
More fixes, changes and workarounds for indentation problems.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95607 - Directory Listing
Modified Wed Aug 13 14:09:41 2014 UTC (5 years, 3 months ago) by apaolo

Fixed bug/inconsistenty in class EIFFEL_LIST. A feature named `index' is inherited from both ancestors. Only one of them is effective, so the features are merged, but this is inconsistent, as they have different semantics.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95606 - Directory Listing
Modified Wed Aug 13 14:09:07 2014 UTC (5 years, 3 months ago) by apaolo

Finally fixed indentation. Hopefully forever.
-------
Committed by git-svn. Additional info about the commit:
Author: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:49:19 +02:00
Committer: Paolo Antonucci <blackantitoon@gmail.com> @ 12/08/2014 21:50:09 +02:00

---

Revision 95604 - Directory Listing
Modified Tue Aug 12 17:08:39 2014 UTC (5 years, 3 months ago) by polikarn

Multiple changes to make AutoProof more predictable on big examples (simplified/optimized base theory, simplified type properties, inlined some checks, no generation of triggers by default, removed unused locals, strengthened inheritance axioms, new mechanism for type properties in logic classes, adjustible default update guards). Allow lemmas in logic classes. Bugfixes (including an unsound axiom for partial invariants).

---

Revision 95588 - Directory Listing
Modified Fri Aug 8 09:44:13 2014 UTC (5 years, 4 months ago) by jasonw

<<Merged from trunk#95587.>>

---

Revision 95576 - Directory Listing
Modified Tue Aug 5 11:31:08 2014 UTC (5 years, 4 months ago) by maxpei

Fixed a bug in AutoTest which led to invalid file name for the new root class on Linux.

---

Revision 95575 - Directory Listing
Modified Tue Aug 5 07:53:40 2014 UTC (5 years, 4 months ago) by maxpei

Forced termination of external processes at the end of testing/fixing.

---

Revision 95574 - Directory Listing
Modified Tue Aug 5 07:52:39 2014 UTC (5 years, 4 months ago) by maxpei

Removed the minimum width constraint for GUI widgets in AutoFix.

---

Revision 95573 - Directory Listing
Modified Tue Aug 5 07:51:08 2014 UTC (5 years, 4 months ago) by maxpei

Reconstructed the feature text before/after a fix to implementation so that the feature header comments are preserved.

---

Revision 95569 - Directory Listing
Modified Fri Aug 1 18:07:17 2014 UTC (5 years, 4 months ago) by apaolo

Fixed batch target. I broke it one month and a half ago by accidentally removing the code_analysis library. Sorry!

---

Revision 95543 - Directory Listing
Modified Thu Jul 31 07:37:41 2014 UTC (5 years, 4 months ago) by maxpei

Fixed a bug in AutoDebug which prevents a continuous AutoFixing session from being stopped.
Improved the navigation between faults and fixes via double clicking on grid rows.

---

Revision 95539 - Directory Listing
Modified Tue Jul 29 21:27:41 2014 UTC (5 years, 4 months ago) by maxpei

Fixed a bug in AutoTest that may cause Void-call-target errors.

---

Revision 95528 - Directory Listing
Modified Mon Jul 28 13:20:57 2014 UTC (5 years, 4 months ago) by polikarn

Fixed in_domain frame axiom trigger; generating triggers only in class invariants; changed model of V_SEQUENCE to sequence.

---

Revision 95505 - Directory Listing
Modified Thu Jul 24 11:02:02 2014 UTC (5 years, 4 months ago) by maxpei

AutoDebug: fixed a bug in invoking AutoTest with a given seed;
AutoDebug: changed the fixing process to start with making a new copy of the project.
AutoFix: construct also boolean-valued calls like Current.feature_name (Int) for state monitoring.
AutoFix: execution traces may get modified during impl-fixing, causing the following contract-fixing to fail; Now we create a deep copy of the traces for later use.

---

Revision 95497 - Directory Listing
Modified Wed Jul 23 20:36:25 2014 UTC (5 years, 4 months ago) by polikarn

Bugfix: redefined query types in abstract frames.

---

Revision 95478 - Directory Listing
Modified Tue Jul 22 17:05:02 2014 UTC (5 years, 4 months ago) by polikarn

Fixed verification time reporting. Removed numeric properties when overflow is not checked.

---

Revision 95477 - Directory Listing
Modified Tue Jul 22 11:55:56 2014 UTC (5 years, 4 months ago) by polikarn

Added option for (not) generating triggers. Changed framing in base theory the way Rustan suggested. Added dir-level options to testing script.

---

Revision 95476 - Directory Listing
Modified Tue Jul 22 11:15:09 2014 UTC (5 years, 4 months ago) by maxpei

Fixed a fault that will cause non-AutoFixable faults to be hidden on the Faults panel.
Fixed the fault of reporting more than max number of fixes to contracts.

---

Revision 95475 - Directory Listing
Modified Tue Jul 22 09:24:52 2014 UTC (5 years, 4 months ago) by polikarn

Bugfix.

---

Revision 95474 - Directory Listing
Modified Tue Jul 22 08:59:37 2014 UTC (5 years, 4 months ago) by polikarn

Simplified partial contracts. Introducing extra bound vars to replace arithmetic in quantifiers (alternative to triggering on arithmetic).

---

Revision 95469 - Directory Listing
Modified Mon Jul 21 14:22:58 2014 UTC (5 years, 4 months ago) by maxpei

Fixed a few bugs in AutoDebug.

---

Revision 95468 - Directory Listing
Modified Sun Jul 20 09:11:06 2014 UTC (5 years, 4 months ago) by schmisam

Added code analysis rule for comparison of object references.
Added test for the rule.
Some beautification of older rules.

---

Revision 95467 - Directory Listing
Modified Sun Jul 20 07:49:56 2014 UTC (5 years, 4 months ago) by schmisam

Added code analysis rule for Void checking using 'is_equal'
Added test for this rule.

---

Revision 95466 - Directory Listing
Modified Sat Jul 19 21:50:46 2014 UTC (5 years, 4 months ago) by schmisam

Added code analysis rule for empty creation procedures without arguments.
Added test for this rule.

---

Revision 95465 - Directory Listing
Modified Sat Jul 19 15:10:12 2014 UTC (5 years, 4 months ago) by schmisam

Added code analysis rule for creation of objects in loops
Added tests for the rule.

---

Revision 95462 - Directory Listing
Modified Fri Jul 18 15:26:39 2014 UTC (5 years, 4 months ago) by maxpei

Renamed the AutoDebug tool to AutoFix;
Added support to manual fixes;
Rephrased a few UI strings;

---

Revision 95461 - Directory Listing
Modified Fri Jul 18 15:18:45 2014 UTC (5 years, 4 months ago) by schmisam

Added code analysis rule for not well phrased comments.
Added tests for this rule.

---

Revision 95442 - Directory Listing
Modified Thu Jul 17 13:27:51 2014 UTC (5 years, 4 months ago) by schmisam

Added rule for missing creation procedures with no arguments
Added tests for said rule.

---

Revision 95440 - Directory Listing
Modified Thu Jul 17 00:25:44 2014 UTC (5 years, 4 months ago) by schmisam

Added code analysis rule for empty loops.
Added tests for empty loops.

---

Revision 95429 - Directory Listing
Modified Wed Jul 16 12:44:38 2014 UTC (5 years, 4 months ago) by schmisam

Added code analysis rule for double negation.
Added tests for double negation.
Renamed test folder for inherit from any rule to represent rule ID correctly.

---

Revision 95411 - Directory Listing
Modified Mon Jul 14 17:00:46 2014 UTC (5 years, 4 months ago) by manus

Merged revision 95400,95403,95405,95406,95407 from trunk
* Fixed crash in outgoing PDF links.
* Fixed `fix' contextual menu that was not doing anything in error tool panel
* Cosmetics: hide flashing scrollbar in confirmation save dialog for unsaved classes.
* Cosmetics: menu entries are not truncated anymore
* Less flashing over remote desktop/citrix session when using completion window.

---

Revision 95408 - Directory Listing
Modified Sun Jul 13 13:19:40 2014 UTC (5 years, 4 months ago) by apaolo

The last commit did not compile, most likely due to being based on an outdated working copy. Fixed.

---

Revision 95402 - Directory Listing
Modified Fri Jul 11 18:34:35 2014 UTC (5 years, 5 months ago) by schmisam

Added code analysis rule for undesirable comment content.
Added code analysis rule for unnecessary inheritance from ANY (work in progress).
Added tests for the new rules.

---

Revision 95399 - Directory Listing
Modified Fri Jul 11 06:52:37 2014 UTC (5 years, 5 months ago) by jasonw

<<Merged from trunk#95398.>>

---

Revision 95394 - Directory Listing
Modified Wed Jul 9 23:41:36 2014 UTC (5 years, 5 months ago) by manus

Merged the following revisions: 95213,95215,95216,95235,95236,95237,95253,95255,95261,95262,95263,95264,95279,95280,95281,95282,95294,95297,95298,95300,95301,95305,95312,95314,95315,95327,95328,95329,95330,95335,95339,95340,95347,95379,95383,95387:
* Fixed issues with QAT
* Fixed issue with .NET 4.0 consuming COM wrapped classes
* Use different port number for attaching a debugger
* Better type suggestion for type inference
* Improved code analysis command line options

---

Revision 95358 - Directory Listing
Modified Fri Jul 4 10:11:56 2014 UTC (5 years, 5 months ago) by jasonw

<<Merged from trunk#95357.>>

---

Revision 95346 - Directory Listing
Modified Tue Jul 1 19:19:20 2014 UTC (5 years, 5 months ago) by alexk

Added C++ compilation flags and new object files that are part of the new SCOOP implementation.

---

Revision 95345 - Directory Listing
Modified Tue Jul 1 19:17:51 2014 UTC (5 years, 5 months ago) by alexk

Changed declaration of an atomic variable to be able to initialize it using an aggregate initializer (the restriction is imposed by Visual Studio).
Protected call to "exft" that is not available in workbench mode.

---

Revision 95344 - Directory Listing
Modified Tue Jul 1 19:14:16 2014 UTC (5 years, 5 months ago) by alexk

Avoided an error reported for comparing a pointer to 0 because the comparison is ambiguous.

---

Revision 95343 - Directory Listing
Modified Tue Jul 1 19:12:05 2014 UTC (5 years, 5 months ago) by alexk

Avoided unused local variable report when compiling without assertions.

---

Revision 95342 - Directory Listing
Modified Tue Jul 1 19:10:50 2014 UTC (5 years, 5 months ago) by alexk

Added C++ compiler flags.

---

Revision 95332 - Directory Listing
Modified Fri Jun 27 12:57:49 2014 UTC (5 years, 5 months ago) by maxpei

Fixed a few bugs in AutoFix and AutoDebug.

---

Revision 95331 - Directory Listing
Modified Fri Jun 27 08:57:34 2014 UTC (5 years, 5 months ago) by jasonw

<<Merged from trunk#95330.>>

---

Revision 95320 - Directory Listing
Modified Sat Jun 21 22:38:32 2014 UTC (5 years, 5 months ago) by maxpei

AutoDebug 0.0.1

---

Revision 95317 - Directory Listing
Modified Fri Jun 20 13:55:59 2014 UTC (5 years, 5 months ago) by apaolo

Replaced double quotes with single quotes in some rule preferences, as double quotes create parsing problems from the command line.

Rule "Empty uncommented routine" now also checks that the body of features does not contain any comment. If it does, then it is probably intended to leave the implementation empty and a violation is not triggered.

---

Revision 95274 - Directory Listing
Modified Tue Jun 17 21:59:04 2014 UTC (5 years, 5 months ago) by apaolo

Several small changes and code cleanup.

---

Revision 95273 - Directory Listing
Modified Tue Jun 17 21:58:15 2014 UTC (5 years, 5 months ago) by apaolo

Hint parsing works properly!

---

Revision 95272 - Directory Listing
Modified Tue Jun 17 21:57:42 2014 UTC (5 years, 5 months ago) by apaolo

Hopefully proper and consistent handling of indentation and blank lines. (this was very tiring!)
Right now, comments starting with "-- #HINT" are output, the others are filtered away.

---

Revision 95271 - Directory Listing
Modified Tue Jun 17 21:57:06 2014 UTC (5 years, 5 months ago) by apaolo

Handling of indentation and blank lines (still work in progress).

---

Revision 95270 - Directory Listing
Modified Tue Jun 17 21:56:30 2014 UTC (5 years, 5 months ago) by apaolo

AutoTeach Hinter: now able to succesfully output a class text removing the routine bodies (but preserving the comments inside them).

---

Revision 95269 - Directory Listing
Modified Tue Jun 17 21:56:00 2014 UTC (5 years, 5 months ago) by apaolo

Now able to only print comments in a class.

---

Revision 95268 - Directory Listing
Modified Tue Jun 17 21:55:28 2014 UTC (5 years, 5 months ago) by apaolo

Getting closer to the actual class processing.

---

Revision 95267 - Directory Listing
Modified Tue Jun 17 21:54:51 2014 UTC (5 years, 5 months ago) by apaolo

More work on the command line.

---

Revision 95266 - Directory Listing
Modified Tue Jun 17 21:54:13 2014 UTC (5 years, 5 months ago) by apaolo

AutoTeach: command line argument parsing.

---

Revision 95265 - Directory Listing
Modified Tue Jun 17 21:53:29 2014 UTC (5 years, 5 months ago) by apaolo

Creating new AutoTeach tool and skeleton of AutoTeach command line command.
Added skeleton of the initial "Hinter" component (better names wanted!), taking example from the command line version of the Code Analysis tool.

Conflicts:
	Eiffel/Ace/ec.ecf

---

Revision 95254 - Directory Listing
Modified Fri Jun 13 16:49:14 2014 UTC (5 years, 5 months ago) by alexeyk

void-safety fixes for testing.ecf project.
Reason: manual testing is not working for fresh projects, compiled with EVE version of testing.ecf
There are still 38 errors to fix.

---

Revision 95252 - Directory Listing
Modified Fri Jun 13 08:20:35 2014 UTC (5 years, 5 months ago) by jasonw

<<Merged from trunk#95251.>>

---

Revision 95241 - Directory Listing
Modified Wed Jun 11 16:47:03 2014 UTC (5 years, 6 months ago) by apaolo

All concerns raised in the code review should now have been addressed.

---

Revision 95240 - Directory Listing
Modified Wed Jun 11 16:45:55 2014 UTC (5 years, 6 months ago) by apaolo

Fixed code review comments. Amend me!

---

Revision 95239 - Directory Listing
Modified Wed Jun 11 16:44:50 2014 UTC (5 years, 6 months ago) by apaolo

Fixed some of the concerns raised in the code review (minor changes).

---

Revision 95238 - Directory Listing
Modified Wed Jun 11 16:44:01 2014 UTC (5 years, 6 months ago) by apaolo

Fixed double 'elseif' block for "-code-analysis" when checking command line argument.

This seems to be an oversight introduced in a merge from the trunk to the EVE branch.

---

Revision 95232 - Directory Listing
Modified Fri Jun 6 08:51:38 2014 UTC (5 years, 6 months ago) by jasonw

<<Merged from trunk#95231.>>

---

Revision 95217 - Directory Listing
Modified Mon Jun 2 17:51:34 2014 UTC (5 years, 6 months ago) by manus

We now do the raspberry pi delivery automatically.

---

Revision 95211 - Directory Listing
Modified Fri May 30 23:54:39 2014 UTC (5 years, 6 months ago) by manus

Updated to 14.05 branch.

---

Revision 95210 - Directory Listing
Modified Fri May 30 23:36:09 2014 UTC (5 years, 6 months ago) by manus

Updated to the 14.05 branch.

---

Revision 95205 - Directory Listing
Modified Fri May 30 15:51:18 2014 UTC (5 years, 6 months ago) by manus

Added updated Chinese translation.

---

Revision 95203 - Directory Listing
Modified Fri May 30 08:05:42 2014 UTC (5 years, 6 months ago) by jasonw

<<Merged from trunk#95202.>>

---

Revision 95201 - Directory Listing
Modified Thu May 29 23:49:54 2014 UTC (5 years, 6 months ago) by manus

Created the 14.05 release branch.

---

Revision 95200 - Directory Listing
Modified Thu May 29 23:49:30 2014 UTC (5 years, 6 months ago) by manus

Removed.

---

Revision 95199 - Directory Listing
Modified Thu May 29 23:48:38 2014 UTC (5 years, 6 months ago) by manus

Created the 14.05 release branch.

---

Revision 95176 - Directory Listing
Modified Mon May 26 08:24:19 2014 UTC (5 years, 6 months ago) by maxpei

AutoDebug reporting list of faults found during testing.

---

Revision 94994 - Directory Listing
Modified Mon May 5 22:28:03 2014 UTC (5 years, 7 months ago) by erudel

Added Eiffel linear programming library and constraint-based layout manager

---

Revision 94983 - Directory Listing
Modified Fri May 2 11:05:28 2014 UTC (5 years, 7 months ago) by jasonw

<<Merged from trunk#94978.>>

---

Revision 94905 - Directory Listing
Modified Tue Apr 22 09:14:44 2014 UTC (5 years, 7 months ago) by mschill

Fixed bug in replace feature

---

Revision 94904 - Directory Listing
Modified Tue Apr 22 09:12:46 2014 UTC (5 years, 7 months ago) by mschill

Added basic file system support

---

Revision 94899 - Directory Listing
Modified Sun Apr 20 16:39:38 2014 UTC (5 years, 7 months ago) by polikarn

Conversion of manifest arrays into sequences.

---

Revision 94896 - Directory Listing
Modified Fri Apr 18 18:57:57 2014 UTC (5 years, 7 months ago) by polikarn

Added array_sum example.

---

Revision 94895 - Directory Listing
Modified Fri Apr 18 18:32:47 2014 UTC (5 years, 7 months ago) by polikarn

Added dll example to comcom directory.

---

Revision 94892 - Directory Listing
Modified Fri Apr 18 18:11:35 2014 UTC (5 years, 7 months ago) by polikarn

Adding arrays.bpl through theory mechanism instead of hard coded. Added V_ARRAY class to use in verification (arrays.bpl deos not always work). Added comcom examples to tests.

---

Revision 94891 - Directory Listing
Modified Fri Apr 18 16:59:55 2014 UTC (5 years, 7 months ago) by polikarn

Changed tuple encoding (generating Boogie type per tuple type). Fixed bug with default loop varaints with reference exit conditions.

---

Revision 94885 - Directory Listing
Modified Thu Apr 17 17:06:14 2014 UTC (5 years, 7 months ago) by polikarn

Bringing in invariants of closed objects automatically unless manual_inv: true is specified.

---

Revision 94877 - Directory Listing
Modified Wed Apr 16 17:59:21 2014 UTC (5 years, 7 months ago) by apaolo

Properly renamed all occurrences of "Empty uncommented feature" to "Empty uncommented routine".

---

Revision 94875 - Directory Listing
Modified Wed Apr 16 17:42:14 2014 UTC (5 years, 7 months ago) by apaolo

Rearranged Paolo's Inspector Eiffel rules into the proper folders.
Deleted incomplete rule "Attribute should be local" as a very similar one (CA064) already exists.

---

Revision 94874 - Directory Listing
Modified Wed Apr 16 17:40:57 2014 UTC (5 years, 7 months ago) by apaolo

Several small fixes and improvements to Inspector Eiffel rules.

- No CA_MISC_UTILS class anymore, {STRING}.adjust can be used instead of the helper trim_string function.
- Added option to the Argument and local variable naming convention rules for checking for the 'a_' and 'l_' prefix.
- In "Mergeable feature clauses" rule, uncommented feature clauses are now ignored (a rule which complains about these already exists)
- "Unneeded accessor function" rule is now always triggered regardless of the attribute export status
- Fixed subtle bug in "Explicit redundant inheritance" rule. It seems that {ARRAYED_LIST}.merge_right also erases the source sequence.

---

Revision 94873 - Directory Listing
Modified Wed Apr 16 17:40:07 2014 UTC (5 years, 7 months ago) by apaolo

Implemented new "Inspect instruction has no 'when' branch" and "Explicit redundant inheritance" Inspector Eiffel rules.

---

Revision 94869 - Directory Listing
Modified Wed Apr 16 16:21:32 2014 UTC (5 years, 7 months ago) by apaolo

Added skeletons for three new Inspector Eiffel rules + file renaming and prettification.

---

Revision 94868 - Directory Listing
Modified Wed Apr 16 16:20:32 2014 UTC (5 years, 7 months ago) by apaolo

Added new "Empty rescue clause" Inspector Eiffel rule.

---

Revision 94867 - Directory Listing
Modified Wed Apr 16 16:19:51 2014 UTC (5 years, 7 months ago) by apaolo

Minor changes to some Inspector Eiffel rules.

---

Revision 94866 - Directory Listing
Modified Wed Apr 16 16:19:10 2014 UTC (5 years, 7 months ago) by apaolo

Added new "Mergeable feature clauses" Inspector Eiffel rule. Added new class.CA_MISC_UTILS class.

---

Revision 94865 - Directory Listing
Modified Wed Apr 16 16:18:27 2014 UTC (5 years, 7 months ago) by apaolo

Improved rules about naming conventions: they are now able to actually check the identifiers' case.

---

Revision 94864 - Directory Listing
Modified Wed Apr 16 16:17:49 2014 UTC (5 years, 7 months ago) by apaolo

Renamed and improved "Unnecessary sign operator" Inspector Eiffel rule.

---

Revision 94863 - Directory Listing
Modified Wed Apr 16 16:17:11 2014 UTC (5 years, 7 months ago) by apaolo

Added new 'Unneeded accessor function' rule for Inspector Eiffel (and some class prettification).

---

Revision 94862 - Directory Listing
Modified Wed Apr 16 16:16:29 2014 UTC (5 years, 7 months ago) by apaolo

Added new 'Empty uncommented feature' rule for Inspector Eiffel.

---

Revision 94861 - Directory Listing
Modified Wed Apr 16 16:15:49 2014 UTC (5 years, 7 months ago) by apaolo

Adding new rules about naming conventions and unnecessary unary operators.

---

Revision 94831 - Directory Listing
Modified Fri Apr 11 16:39:21 2014 UTC (5 years, 8 months ago) by polikarn

LINKED_LIST verifies again (LINKED_STACK does not).

---

Revision 94810 - Directory Listing
Modified Thu Apr 10 16:41:28 2014 UTC (5 years, 8 months ago) by polikarn

Added DISPENSER, STACK and LINKED_STACK.

---

Revision 94804 - Directory Listing
Modified Wed Apr 9 15:51:51 2014 UTC (5 years, 8 months ago) by polikarn

Bugfix: lemma calls in loops. Added bag-based spec for LIST.remove, LIST.remove_all.

---

Revision 94799 - Directory Listing
Modified Wed Apr 9 13:12:36 2014 UTC (5 years, 8 months ago) by polikarn

Type properties for locals.

---

Revision 94797 - Directory Listing
Modified Wed Apr 9 11:27:24 2014 UTC (5 years, 8 months ago) by polikarn

Implemented opaque functions (definition triggered explicitly)

---

Revision 94786 - Directory Listing
Modified Mon Apr 7 12:44:22 2014 UTC (5 years, 8 months ago) by polikarn

Complete verification up to LINKED_LIST, expect merge_after and reverse.

---

Revision 94785 - Directory Listing
Modified Sun Apr 6 16:45:39 2014 UTC (5 years, 8 months ago) by polikarn

Changed default trigger generation not to use binary/unary operations in function arguments.

---

Revision 94783 - Directory Listing
Modified Fri Apr 4 15:11:06 2014 UTC (5 years, 8 months ago) by polikarn

Verified linked list + iterator, except 4 routines.

---

Revision 94782 - Directory Listing
Modified Fri Apr 4 14:36:31 2014 UTC (5 years, 8 months ago) by julian

Verification assistant: ignore AutoTest root class.

---

Revision 94779 - Directory Listing
Modified Fri Apr 4 13:12:48 2014 UTC (5 years, 8 months ago) by polikarn

Allowing to mention tags of default invariant clauses in inv_only and inv_without.

---

Revision 94778 - Directory Listing
Modified Fri Apr 4 13:05:03 2014 UTC (5 years, 8 months ago) by julian

AutoProof: two-step verification now ignores invariant admissibility.

---

Revision 94777 - Directory Listing
Modified Fri Apr 4 09:12:40 2014 UTC (5 years, 8 months ago) by julian

Fixed bug when launching test sessions.

---

Revision 94773 - Directory Listing
Modified Thu Apr 3 17:19:35 2014 UTC (5 years, 8 months ago) by polikarn

Optimized invariants with repeated inheritance.

---

Revision 94772 - Directory Listing
Modified Thu Apr 3 14:26:37 2014 UTC (5 years, 8 months ago) by polikarn

Further fix of calculating replaced model queries.

---

Revision 94771 - Directory Listing
Modified Thu Apr 3 12:37:44 2014 UTC (5 years, 8 months ago) by polikarn

Bugfix: redefinitions now taken into account when calculating replaced model queries.

---

Revision 94766 - Directory Listing
Modified Wed Apr 2 09:48:14 2014 UTC (5 years, 8 months ago) by apaolo

Revert "Hopefully the last test commit for git-svn, sorry!"

This reverts commit e00eaf3b1be408a8049dcff577cef63a17246350.

---

Revision 94765 - Directory Listing
Modified Wed Apr 2 09:46:29 2014 UTC (5 years, 8 months ago) by apaolo

Hopefully the last test commit for git-svn, sorry!

---

Revision 94757 - Directory Listing
Modified Tue Apr 1 15:36:01 2014 UTC (5 years, 8 months ago) by polikarn

Changed implicit attribute update to check modify clause instead of writable. Fixed initialization issues.

---

Revision 94755 - Directory Listing
Modified Tue Apr 1 07:29:28 2014 UTC (5 years, 8 months ago) by julian

AutoProof: fixed two-step verification and inlining.

---

Revision 94746 - Directory Listing
Modified Mon Mar 31 16:35:58 2014 UTC (5 years, 8 months ago) by apaolo

Undo test commit.

---

Revision 94745 - Directory Listing
Modified Mon Mar 31 16:35:20 2014 UTC (5 years, 8 months ago) by apaolo

Test commit

---

Revision 94744 - Directory Listing
Modified Sun Mar 30 18:26:04 2014 UTC (5 years, 8 months ago) by julian

verification assistant: fixed crash on empty clusters

---

Revision 94740 - Directory Listing
Modified Fri Mar 28 09:42:08 2014 UTC (5 years, 8 months ago) by jasonw

<<Merged from trunk#94739.>>

---

Revision 94732 - Directory Listing
Modified Thu Mar 27 15:31:03 2014 UTC (5 years, 8 months ago) by mschill

Fixed substring, added merge 

---

Revision 94678 - Directory Listing
Modified Mon Mar 24 14:24:24 2014 UTC (5 years, 8 months ago) by mschill

Fixed some issues when reading empty files

---

Revision 94664 - Directory Listing
Modified Fri Mar 21 16:40:01 2014 UTC (5 years, 8 months ago) by julian

Verification Assistant: added status messages for running tools.

---

Revision 94663 - Directory Listing
Modified Fri Mar 21 07:52:56 2014 UTC (5 years, 8 months ago) by jasonw

<<Merged from trunk#94661.>>

---

Revision 94655 - Directory Listing
Modified Thu Mar 20 15:51:35 2014 UTC (5 years, 8 months ago) by manus

Moved the code analysis framework to trunk.

---

Revision 94654 - Directory Listing
Modified Thu Mar 20 13:50:59 2014 UTC (5 years, 8 months ago) by zurfluhs

Code Analysis: updated tool name in cmd mode

---

Revision 94653 - Directory Listing
Modified Thu Mar 20 12:44:38 2014 UTC (5 years, 8 months ago) by zurfluhs

Code Analysis: introduced new tool name "Inspector Eiffel"

---

Revision 94615 - Directory Listing
Modified Tue Mar 18 11:23:38 2014 UTC (5 years, 8 months ago) by mschill

Fixed bug in case of closed connections and added some comments.

---

Revision 94608 - Directory Listing
Modified Mon Mar 17 14:29:07 2014 UTC (5 years, 8 months ago) by julian

AutoProof: fixed bug in Boogie output parser.

---

Revision 94606 - Directory Listing
Modified Sun Mar 16 11:15:00 2014 UTC (5 years, 8 months ago) by polikarn

Implemented implicit model queries.

---

Revision 94605 - Directory Listing
Modified Sun Mar 16 09:38:04 2014 UTC (5 years, 8 months ago) by polikarn

Introduced Default value function to be used on creation.

---

Revision 94604 - Directory Listing
Modified Sat Mar 15 14:57:57 2014 UTC (5 years, 8 months ago) by polikarn

Removed an unsoundness caused by merging attributes with multiple inheritance. Fixed bug with frozen types vs. frozen classes.

---

Revision 94603 - Directory Listing
Modified Fri Mar 14 18:21:48 2014 UTC (5 years, 8 months ago) by polikarn

Removed global_public (super slow) and added annotations as a consequence; reseting type/var counters after every verification; changed EB2 specs to verify with the sound invariant frame axiom.

---

Revision 94599 - Directory Listing
Modified Fri Mar 14 13:21:17 2014 UTC (5 years, 8 months ago) by polikarn

Added test script for base2.

---

Revision 94598 - Directory Listing
Modified Fri Mar 14 12:30:12 2014 UTC (5 years, 8 months ago) by polikarn

Fixed tests: more restrictive trigger for invariant frame axiom + new PIP results.

---

Revision 94597 - Directory Listing
Modified Thu Mar 13 15:47:34 2014 UTC (5 years, 8 months ago) by apaolo

Undoing test commit

---

Revision 94596 - Directory Listing
Modified Thu Mar 13 15:42:34 2014 UTC (5 years, 8 months ago) by apaolo

Test

---

Revision 94595 - Directory Listing
Modified Thu Mar 13 13:16:00 2014 UTC (5 years, 8 months ago) by maxpei

Added the missing (from last commit) class necessary for AutoFix.

---

Revision 94594 - Directory Listing
Modified Thu Mar 13 13:12:57 2014 UTC (5 years, 8 months ago) by maxpei

Refactored/Cleaned AutoFix and SpeciFix.

---

Revision 94593 - Directory Listing
Modified Thu Mar 13 12:03:58 2014 UTC (5 years, 8 months ago) by maxpei

Changed the location to save the generated testing root class: now it is stored in the same dir as the project root class.

---

Revision 94588 - Directory Listing
Modified Wed Mar 12 11:39:02 2014 UTC (5 years, 9 months ago) by zurfluhs

Code Analysis: command-line option '-caloadprefs'

---

Revision 94587 - Directory Listing
Modified Wed Mar 12 10:36:13 2014 UTC (5 years, 9 months ago) by zurfluhs

Code Analysis: bugfix + comments

---

Revision 94586 - Directory Listing
Modified Tue Mar 11 15:41:40 2014 UTC (5 years, 9 months ago) by julian

Fixed integration of AutoProof to Verification Assistant.

---

Revision 94583 - Directory Listing
Modified Mon Mar 10 12:22:52 2014 UTC (5 years, 9 months ago) by julian

Cleaned up code analysis ecf file.

---

Revision 94582 - Directory Listing
Modified Sun Mar 9 15:37:33 2014 UTC (5 years, 9 months ago) by polikarn

Bugfix: well-formedness checks inside old expressions. Fixed the unsound frame axiom for class invariants.

---

Revision 94581 - Directory Listing
Modified Fri Mar 7 11:57:58 2014 UTC (5 years, 9 months ago) by jasonw

<<Merged from trunk#94580.>>

---

Revision 94579 - Directory Listing
Modified Thu Mar 6 13:37:57 2014 UTC (5 years, 9 months ago) by zurfluhs

Code Analysis: comments

---

Revision 94578 - Directory Listing
Modified Thu Mar 6 13:36:14 2014 UTC (5 years, 9 months ago) by zurfluhs

Code Analysis: comments

---

Revision 94577 - Directory Listing
Modified Thu Mar 6 11:40:34 2014 UTC (5 years, 9 months ago) by mschill

Added string searcher again

---

Revision 94556 - Directory Listing
Modified Fri Feb 28 09:44:00 2014 UTC (5 years, 9 months ago) by jasonw

<<Merged from trunk#94547.>>

---

Revision 94555 - Directory Listing
Modified Fri Feb 28 09:38:22 2014 UTC (5 years, 9 months ago) by mschill

Bug fixes

---

Revision 94536 - Directory Listing
Modified Thu Feb 27 14:16:46 2014 UTC (5 years, 9 months ago) by julian

AutoProof: improve feedback during verification.

---

Revision 94505 - Directory Listing
Modified Mon Feb 24 16:14:14 2014 UTC (5 years, 9 months ago) by polikarn

Simplified PIP specs/updated some specs.

---

Revision 94502 - Directory Listing
Modified Mon Feb 24 13:30:15 2014 UTC (5 years, 9 months ago) by julian

AutoProof: improve feedback during verification.

---

Revision 94498 - Directory Listing
Modified Mon Feb 24 12:08:17 2014 UTC (5 years, 9 months ago) by zurfluhs

Code Analysis: refactoring

---

Revision 94496 - Directory Listing
Modified Mon Feb 24 11:59:28 2014 UTC (5 years, 9 months ago) by zurfluhs

Code Analysis: refactoring

---

Revision 94495 - Directory Listing
Modified Mon Feb 24 08:56:09 2014 UTC (5 years, 9 months ago) by polikarn

Real triggering on partial invariants. Framing for domains. Bugfix for redefining functions into attributes.

---

Revision 94494 - Directory Listing
Modified Sun Feb 23 22:43:11 2014 UTC (5 years, 9 months ago) by julian

AutoProof: update to PIP.

---

Revision 94493 - Directory Listing
Modified Sun Feb 23 19:21:00 2014 UTC (5 years, 9 months ago) by julian

AutoProof: added new PIP version.

---

Revision 94492 - Directory Listing
Modified Sat Feb 22 17:22:35 2014 UTC (5 years, 9 months ago) by polikarn

Verified CELL_CURSOR. Minor bugfix. Renamed ghost index.

---

Revision 94491 - Directory Listing
Modified Sat Feb 22 16:35:51 2014 UTC (5 years, 9 months ago) by polikarn

Simple solution for trigerring partial invariants. Simplified some specs.

---

Revision 94461 - Directory Listing
Modified Fri Feb 21 15:39:42 2014 UTC (5 years, 9 months ago) by polikarn

Fixes in model replacement mechanism. Verified LIST (except remove, remove_all). Cleaned up base2.

---

Revision 94460 - Directory Listing
Modified Fri Feb 21 15:16:23 2014 UTC (5 years, 9 months ago) by alexeyk

typo in comment

---

Revision 94459 - Directory Listing
Modified Fri Feb 21 14:16:42 2014 UTC (5 years, 9 months ago) by mschill

Added comments and removed unused code

---

Revision 94458 - Directory Listing
Modified Fri Feb 21 14:03:09 2014 UTC (5 years, 9 months ago) by mschill

Major update to networking, expanded strings and nspr libraries

---

Revision 94428 - Directory Listing
Modified Thu Feb 20 19:23:06 2014 UTC (5 years, 9 months ago) by polikarn

Fixed test output.

---

Revision 94427 - Directory Listing
Modified Thu Feb 20 19:18:16 2014 UTC (5 years, 9 months ago) by polikarn

Closing abstract frames under model replacements; checking that replacing models are new.

---

Revision 94357 - Directory Listing
Modified Tue Feb 18 17:04:26 2014 UTC (5 years, 9 months ago) by polikarn

Minor bugfix.

---

Revision 94356 - Directory Listing
Modified Tue Feb 18 16:56:47 2014 UTC (5 years, 9 months ago) by julian

AutoProof: Improve translation speed by caching map features.
AutoProof: Improve translation speed by only compiling on workbench changes.

---

Revision 94350 - Directory Listing
Modified Mon Feb 17 20:52:50 2014 UTC (5 years, 9 months ago) by polikarn

Added CELL and LINKABLE.

---

Revision 94341 - Directory Listing
Modified Mon Feb 17 13:06:39 2014 UTC (5 years, 9 months ago) by polikarn

Checking frame redefinitions.

---

Revision 94336 - Directory Listing
Modified Sun Feb 16 18:14:07 2014 UTC (5 years, 9 months ago) by polikarn

Chnged semantics of read clauses to exclude ownership domains.

---

Revision 94335 - Directory Listing
Modified Sun Feb 16 17:31:43 2014 UTC (5 years, 9 months ago) by polikarn

Edited uncompiled classes + minor fix.

---

Revision 94334 - Directory Listing
Modified Sun Feb 16 16:53:58 2014 UTC (5 years, 9 months ago) by polikarn

Implemented update guards.

---

Revision 94332 - Directory Listing
Modified Sat Feb 15 16:08:53 2014 UTC (5 years, 9 months ago) by polikarn

Adding closed to all model frames.

---

Revision 94307 - Directory Listing
Modified Fri Feb 14 13:39:28 2014 UTC (5 years, 9 months ago) by polikarn

Triggering on arithmetic operations as a command-line option; processing {TYPE}.default_value; verified MUTABLE_SEQUENCE and its iterator.

---

Revision 94288 - Directory Listing
Modified Thu Feb 13 13:30:47 2014 UTC (5 years, 9 months ago) by polikarn

Verified OUTPUT_STREAM and IO_ITERATOR + minor bugfix.

---

Revision 94287 - Directory Listing
Modified Thu Feb 13 13:01:09 2014 UTC (5 years, 9 months ago) by mschill

Fixed clusters (again)

---

Revision 94286 - Directory Listing
Modified Thu Feb 13 12:57:38 2014 UTC (5 years, 9 months ago) by mschill

Fixed cluster location

---

Revision 94285 - Directory Listing
Modified Thu Feb 13 12:51:54 2014 UTC (5 years, 9 months ago) by mschill

Fixed issue in read_line

---

Revision 94284 - Directory Listing
Modified Thu Feb 13 12:39:46 2014 UTC (5 years, 9 months ago) by mschill

Updates for the networking / io library

---

Revision 94273 - Directory Listing
Modified Wed Feb 12 14:36:57 2014 UTC (5 years, 9 months ago) by polikarn

Fixed well-formedness checks in existentials; better approach to triggers; minor bugfixes.

---

Revision 94272 - Directory Listing
Modified Wed Feb 12 14:30:45 2014 UTC (5 years, 9 months ago) by zurfluhs

Code Analysis: refactoring

---

Revision 94271 - Directory Listing
Modified Wed Feb 12 14:28:58 2014 UTC (5 years, 9 months ago) by zurfluhs

Code Analysis: refactoring

---

Revision 94259 - Directory Listing
Modified Tue Feb 11 18:58:20 2014 UTC (5 years, 9 months ago) by zurfluhs

Code Analysis: extracted class for analysis context

- and fixed bug in rule #13

---

Revision 94254 - Directory Listing
Modified Tue Feb 11 08:31:49 2014 UTC (5 years, 9 months ago) by zurfluhs

Code Analysis: refactoring

---

Revision 94252 - Directory Listing
Modified Mon Feb 10 19:40:18 2014 UTC (5 years, 10 months ago) by polikarn

Fixed further typing problems. Verified SEQUENCE_ITERATOR.

---

Revision 94249 - Directory Listing
Modified Mon Feb 10 18:53:59 2014 UTC (5 years, 10 months ago) by polikarn

Fixed some typing issues.

---

Revision 94248 - Directory Listing
Modified Mon Feb 10 15:07:14 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: minor refactoring

---

Revision 94247 - Directory Listing
Modified Mon Feb 10 14:26:56 2014 UTC (5 years, 10 months ago) by polikarn

Verified MAP and MAP_ITERATOR.

---

Revision 94246 - Directory Listing
Modified Mon Feb 10 14:20:43 2014 UTC (5 years, 10 months ago) by polikarn

Generating triggers for across expressions; invariant admissibility is now checked first.

---

Revision 94245 - Directory Listing
Modified Mon Feb 10 13:49:05 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: added exception mechanism during rule checking

---

Revision 94244 - Directory Listing
Modified Sun Feb 9 18:58:57 2014 UTC (5 years, 10 months ago) by polikarn

New approach to abstract framing: model queries are inherited. Big typing refactoring: uniform conversion and type-safe conversion to class types all over the place.

---

Revision 94241 - Directory Listing
Modified Sat Feb 8 13:51:58 2014 UTC (5 years, 10 months ago) by polikarn

Fixed test.

---

Revision 94240 - Directory Listing
Modified Sat Feb 8 13:36:43 2014 UTC (5 years, 10 months ago) by polikarn

Solved the problem with generics by initially instantiating all generic classes with constraints.

---

Revision 94237 - Directory Listing
Modified Fri Feb 7 15:41:22 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: rule #6 bugfix

---

Revision 94236 - Directory Listing
Modified Fri Feb 7 15:30:33 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: rule #34 bugfix

---

Revision 94233 - Directory Listing
Modified Fri Feb 7 13:45:10 2014 UTC (5 years, 10 months ago) by polikarn

Minor bugfix and refactoring.

---

Revision 94232 - Directory Listing
Modified Fri Feb 7 13:04:18 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: minor

---

Revision 94231 - Directory Listing
Modified Fri Feb 7 12:32:22 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: another refactoring

---

Revision 94228 - Directory Listing
Modified Fri Feb 7 06:55:00 2014 UTC (5 years, 10 months ago) by jasonw

<<Merged from trunk#94225.>>

---

Revision 94217 - Directory Listing
Modified Thu Feb 6 16:35:24 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: refactoring

---

Revision 94216 - Directory Listing
Modified Thu Feb 6 15:50:21 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analyzer: control flow graph explanation.

---

Revision 94214 - Directory Listing
Modified Thu Feb 6 15:14:28 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: GUI: text filter

---

Revision 94213 - Directory Listing
Modified Thu Feb 6 14:13:02 2014 UTC (5 years, 10 months ago) by polikarn

Fixed generics test (due to new defaults policy for generic arguments).

---

Revision 94212 - Directory Listing
Modified Thu Feb 6 14:05:02 2014 UTC (5 years, 10 months ago) by polikarn

Freshness. Changed conditions for modifying observers. First 3 classes of EB2 with models.

---

Revision 94211 - Directory Listing
Modified Thu Feb 6 11:26:53 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: redesigned button user interface of tool panel

---

Revision 94210 - Directory Listing
Modified Thu Feb 6 10:22:46 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: changes according to code review

- improved Void-safety
- refactoring of CA_CFG_BUILDER

---

Revision 94209 - Directory Listing
Modified Thu Feb 6 09:34:34 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: slightly new CA_ALL_RULES_CHECKER implementation

---

Revision 94208 - Directory Listing
Modified Thu Feb 6 09:32:00 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: many small improvements

- Void-safety

---

Revision 94194 - Directory Listing
Modified Wed Feb 5 18:28:39 2014 UTC (5 years, 10 months ago) by polikarn

Handling model fields in frames.

---

Revision 94191 - Directory Listing
Modified Wed Feb 5 15:42:52 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: many small improvements

---

Revision 94184 - Directory Listing
Modified Wed Feb 5 10:17:18 2014 UTC (5 years, 10 months ago) by wests

Importing EVE/Qs changes into runtime.

This also adds an ECF/project settings flag that will allow the qs
runtime to be used more easily. Only linux-x86-64 is currently supported.

---

Revision 94168 - Directory Listing
Modified Tue Feb 4 17:11:42 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: minor

---

Revision 94167 - Directory Listing
Modified Tue Feb 4 16:47:25 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: improvements

- GUI colors can be chosen in preferences
- other

---

Revision 94166 - Directory Listing
Modified Tue Feb 4 12:47:30 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: new control flow graph builder

- old one used iterative and recursive procedures
- new one uses visitor pattern

---

Revision 94161 - Directory Listing
Modified Mon Feb 3 14:38:01 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: documentation / Void-safety / refactoring

---

Revision 94160 - Directory Listing
Modified Mon Feb 3 11:59:24 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: type recorder improved

---

Revision 94159 - Directory Listing
Modified Mon Feb 3 11:55:14 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: changes according to code review

---

Revision 94158 - Directory Listing
Modified Mon Feb 3 10:37:52 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: changes according to code review

- renamed CA_LOGGER
- using bottom indices
- removed unneeded Result assigns
- CA_RULE hash code from id
- renamed CA_RULE_VIOLATION.out

---

Revision 94156 - Directory Listing
Modified Sun Feb 2 16:57:38 2014 UTC (5 years, 10 months ago) by polikarn

Verified routines of ITERATOR + minor improvements and bugfixes.

---

Revision 94155 - Directory Listing
Modified Sat Feb 1 16:06:43 2014 UTC (5 years, 10 months ago) by polikarn

A3 checks.

---

Revision 94149 - Directory Listing
Modified Fri Jan 31 17:54:09 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: refactorings and improvements

most importantly:
- status progress during analysis in GUI status bar
- 'short circuit if' bugfix

---

Revision 94147 - Directory Listing
Modified Fri Jan 31 17:08:36 2014 UTC (5 years, 10 months ago) by polikarn

Basic A1 check.

---

Revision 94141 - Directory Listing
Modified Fri Jan 31 14:06:53 2014 UTC (5 years, 10 months ago) by polikarn

Disallowing redefinition of functionals.

---

Revision 94138 - Directory Listing
Modified Fri Jan 31 13:04:58 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: refactoring

- renamed class CA_CFG to CA_CONTROL_FLOW_GRAPH
- removed nonconforming inheritance
- reorganized "rules" folder

---

Revision 94137 - Directory Listing
Modified Fri Jan 31 13:00:31 2014 UTC (5 years, 10 months ago) by polikarn

Made inheritance example work. No default contracts for pure functions. Bugfixes.

---

Revision 94135 - Directory Listing
Modified Fri Jan 31 09:53:46 2014 UTC (5 years, 10 months ago) by julian

EVE: do not initialize blackboard at start.

---

Revision 94134 - Directory Listing
Modified Fri Jan 31 08:25:58 2014 UTC (5 years, 10 months ago) by jasonw

<<Merged from trunk#94133.>>

---

Revision 94130 - Directory Listing
Modified Thu Jan 30 17:50:59 2014 UTC (5 years, 10 months ago) by polikarn

Fixed all tests.

---

Revision 94129 - Directory Listing
Modified Thu Jan 30 14:30:46 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: refactoring / commenting

---

Revision 94127 - Directory Listing
Modified Thu Jan 30 10:17:37 2014 UTC (5 years, 10 months ago) by polikarn

Uniform treatment of partial expressions in contracts (including free preconditions); not all tests pass yet.

---

Revision 94118 - Directory Listing
Modified Wed Jan 29 17:17:19 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: - type information fix - made 'count equals zero' rule safer

---

Revision 94116 - Directory Listing
Modified Wed Jan 29 08:17:23 2014 UTC (5 years, 10 months ago) by mschill

Added a new scoop-compatible networking library

---

Revision 94115 - Directory Listing
Modified Wed Jan 29 08:16:15 2014 UTC (5 years, 10 months ago) by mschill

Added a library for expanded strings

---

Revision 94114 - Directory Listing
Modified Wed Jan 29 08:15:55 2014 UTC (5 years, 10 months ago) by mschill

Added nspr, a library for wrapping the Netscape Portable Runtime

---

Revision 94108 - Directory Listing
Modified Tue Jan 28 18:56:23 2014 UTC (5 years, 10 months ago) by wests

Move SCOOPQS out to the mtlibs section.

---

Revision 94107 - Directory Listing
Modified Tue Jan 28 18:56:00 2014 UTC (5 years, 10 months ago) by wests

Add eif_call_const to SCOOPQS part.

---

Revision 94106 - Directory Listing
Modified Tue Jan 28 15:49:22 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: logging functionality

---

Revision 94104 - Directory Listing
Modified Mon Jan 27 20:22:39 2014 UTC (5 years, 10 months ago) by wests

Makes it possible to compile with EVEQs easier

---

Revision 94102 - Directory Listing
Modified Sat Jan 25 10:18:07 2014 UTC (5 years, 10 months ago) by wests

Reflects API change to RTS_IMPERSONATE

---

Revision 94095 - Directory Listing
Modified Fri Jan 24 18:28:18 2014 UTC (5 years, 10 months ago) by wests

eif_thr_impersonate now takes pids, not objects.

---

Revision 94093 - Directory Listing
Modified Fri Jan 24 16:34:41 2014 UTC (5 years, 10 months ago) by jasonw

<<Merged from trunk#94092.>>

---

Revision 94089 - Directory Listing
Modified Thu Jan 23 21:01:03 2014 UTC (5 years, 10 months ago) by polikarn

More consistent and sound way to handle functional representations of routines (some tests still fail).

---

Revision 94083 - Directory Listing
Modified Wed Jan 22 22:21:00 2014 UTC (5 years, 10 months ago) by wests

Adding uncontrolled check for SCOOPQS

---

Revision 94076 - Directory Listing
Modified Wed Jan 22 19:01:44 2014 UTC (5 years, 10 months ago) by polikarn

Performance optimization.

---

Revision 94075 - Directory Listing
Modified Wed Jan 22 18:08:57 2014 UTC (5 years, 10 months ago) by polikarn

Added read checks.

---

Revision 94068 - Directory Listing
Modified Tue Jan 21 17:50:49 2014 UTC (5 years, 10 months ago) by polikarn

Minor bugfix + test fix.

---

Revision 94067 - Directory Listing
Modified Tue Jan 21 17:30:21 2014 UTC (5 years, 10 months ago) by polikarn

Logical creation in contracts; connecting functional representation to procedure, impure functions; fixing some issues with generics; no built-in set defaults for deferred classes; added first EB2 classes.

---

Revision 94064 - Directory Listing
Modified Mon Jan 20 14:01:25 2014 UTC (5 years, 10 months ago) by polikarn

Added inverse to map; recompiled tests.

---

Revision 94062 - Directory Listing
Modified Mon Jan 20 13:30:47 2014 UTC (5 years, 10 months ago) by polikarn

Added MML_RELATION (+ tests).

---

Revision 94061 - Directory Listing
Modified Sun Jan 19 17:33:06 2014 UTC (5 years, 10 months ago) by polikarn

Added MML_INTERVAL (+ tests).

---

Revision 94060 - Directory Listing
Modified Sun Jan 19 16:43:35 2014 UTC (5 years, 10 months ago) by polikarn

Added MML_MAP (+ tests).

---

Revision 94059 - Directory Listing
Modified Sat Jan 18 16:46:34 2014 UTC (5 years, 10 months ago) by polikarn

Added missed file.

---

Revision 94058 - Directory Listing
Modified Sat Jan 18 16:45:31 2014 UTC (5 years, 10 months ago) by polikarn

Added free invariants to logical types; tests for bags; bugfixes.

---

Revision 94048 - Directory Listing
Modified Fri Jan 17 17:29:10 2014 UTC (5 years, 10 months ago) by polikarn

Added MML_BAG and the corresponding theory (no tests yet).

---

Revision 94046 - Directory Listing
Modified Fri Jan 17 16:15:07 2014 UTC (5 years, 10 months ago) by polikarn

Fixed the rest of the tests.

---

Revision 94040 - Directory Listing
Modified Fri Jan 17 15:28:35 2014 UTC (5 years, 10 months ago) by polikarn

Well-formedness checks inside quantifiers.

---

Revision 94039 - Directory Listing
Modified Fri Jan 17 13:52:23 2014 UTC (5 years, 10 months ago) by polikarn

Unified accross expression handlers.

---

Revision 94038 - Directory Listing
Modified Fri Jan 17 08:52:22 2014 UTC (5 years, 10 months ago) by jasonw

<<Merged from trunk#94035.>>

---

Revision 94029 - Directory Listing
Modified Thu Jan 16 16:22:45 2014 UTC (5 years, 10 months ago) by polikarn

Unified side effects of the two expression translators.

---

Revision 94028 - Directory Listing
Modified Thu Jan 16 14:13:41 2014 UTC (5 years, 10 months ago) by polikarn

Allowing iterable logical types in modify clauses.

---

Revision 94027 - Directory Listing
Modified Thu Jan 16 12:28:06 2014 UTC (5 years, 10 months ago) by polikarn

Mapping termination metric through <= alias.

---

Revision 94026 - Directory Listing
Modified Thu Jan 16 12:03:20 2014 UTC (5 years, 10 months ago) by polikarn

Mapping logical equality through is_equal.

---

Revision 94024 - Directory Listing
Modified Thu Jan 16 07:19:24 2014 UTC (5 years, 10 months ago) by wests

Removing marking from prepare_live_index.

---

Revision 94003 - Directory Listing
Modified Wed Jan 15 17:59:02 2014 UTC (5 years, 10 months ago) by polikarn

Checking preconditions of calls to logicals. Extracting side effects from check instructions. Separated pre- and post-predicate TU.

---

Revision 93999 - Directory Listing
Modified Wed Jan 15 14:09:59 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: small refactoring

---

Revision 93998 - Directory Listing
Modified Wed Jan 15 14:01:51 2014 UTC (5 years, 10 months ago) by julian

AutoProof: fixed real values, fixed GUI crash, updated tests

---

Revision 93997 - Directory Listing
Modified Wed Jan 15 13:45:44 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: refactoring

---

Revision 93996 - Directory Listing
Modified Wed Jan 15 10:20:57 2014 UTC (5 years, 10 months ago) by polikarn

Added expected test output for the framing directory

---

Revision 93995 - Directory Listing
Modified Wed Jan 15 09:56:24 2014 UTC (5 years, 10 months ago) by polikarn

Updated expected test results in advanced directory. Added a dir option to the testing script.

---

Revision 93982 - Directory Listing
Modified Tue Jan 14 14:14:21 2014 UTC (5 years, 10 months ago) by polikarn

Introduced a special type for map with synonyms.

---

Revision 93981 - Directory Listing
Modified Tue Jan 14 13:18:00 2014 UTC (5 years, 10 months ago) by polikarn

Generic mechanism to map logical classes to Boogie map types.

---

Revision 93980 - Directory Listing
Modified Tue Jan 14 12:19:38 2014 UTC (5 years, 10 months ago) by mschill

SCOOP typing exception: Changed note key and improved code

---

Revision 93979 - Directory Listing
Modified Tue Jan 14 11:06:20 2014 UTC (5 years, 10 months ago) by alexk

Moved change-analysis-specific features to change analyzer.

---

Revision 93978 - Directory Listing
Modified Tue Jan 14 03:24:42 2014 UTC (5 years, 10 months ago) by wests

Updating thresh benchmark

---

Revision 93970 - Directory Listing
Modified Mon Jan 13 14:04:09 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: refactoring / small GUI fix

---

Revision 93969 - Directory Listing
Modified Mon Jan 13 12:52:16 2014 UTC (5 years, 10 months ago) by polikarn

Improved error reporting, bugfix in IV_TYPES.

---

Revision 93967 - Directory Listing
Modified Mon Jan 13 12:05:40 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: refactoring

---

Revision 93966 - Directory Listing
Modified Mon Jan 13 09:23:09 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: small improvements

---

Revision 93965 - Directory Listing
Modified Mon Jan 13 07:48:56 2014 UTC (5 years, 10 months ago) by wests

Adding Eve/Qs build option.

This was quite invasive, and I was unable to test all configurations.

---

Revision 93964 - Directory Listing
Modified Sun Jan 12 21:21:15 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: fix

---

Revision 93963 - Directory Listing
Modified Sun Jan 12 19:50:44 2014 UTC (5 years, 10 months ago) by zurfluhs

Code Analysis: comments and some refactoring.

---

Revision 93962 - Directory Listing
Modified Sun Jan 12 19:42:00 2014 UTC (5 years, 10 months ago) by polikarn

Big refactoring: made the IV_TYPE hierarchy more flexible; logical types are not hardcoded, but defined through special note clauses.

---

Revision 93961 - Directory Listing
Modified Sun Jan 12 18:58:57 2014 UTC (5 years, 10 months ago) by wests

Updating SCOOP randmat benchmark

---

Revision 93954 - Directory Listing
Modified Fri Jan 10 14:23:33 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: comments

---

Revision 93953 - Directory Listing
Modified Fri Jan 10 13:55:44 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: refactoring / commenting

---

Revision 93952 - Directory Listing
Modified Fri Jan 10 12:49:55 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: deleted unneeded file

---

Revision 93951 - Directory Listing
Modified Fri Jan 10 12:48:38 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analyzer: refactoring and commenting

---

Revision 93950 - Directory Listing
Modified Fri Jan 10 10:56:52 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: 'unneeded helper' rule

---

Revision 93949 - Directory Listing
Modified Fri Jan 10 09:05:53 2014 UTC (5 years, 11 months ago) by jasonw

<<Merged from trunk#93948.>>

---

Revision 93946 - Directory Listing
Modified Thu Jan 9 17:27:08 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: context menu entry for analyzing cluster

---

Revision 93945 - Directory Listing
Modified Thu Jan 9 17:06:19 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: 'feature never called' rule

- now handles feature with multiple names correctly

---

Revision 93944 - Directory Listing
Modified Thu Jan 9 16:02:21 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: fixes:

- applied fixes are marked and cannot be applied a second time

---

Revision 93943 - Directory Listing
Modified Thu Jan 9 13:38:38 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: 'unneeded helper' rule

---

Revision 93942 - Directory Listing
Modified Thu Jan 9 09:53:26 2014 UTC (5 years, 11 months ago) by polikarn

Moved set and sequence theories to MML. Using note 'theory' to include Boogie files.

---

Revision 93937 - Directory Listing
Modified Wed Jan 8 23:17:55 2014 UTC (5 years, 11 months ago) by manus

Fixed bug#18785 and eweasel test#ccomp089 on Linux 32-bit where our computation of NaN, +Infinity and -Infinity for REAL_32 and REAL_64 was relying on a non-defined behavior of C compilers. Now we use a union type to convert a binary representation of an integer to a float.

---

Revision 93933 - Directory Listing
Modified Wed Jan 8 19:28:53 2014 UTC (5 years, 11 months ago) by manus

Merged from HEAD rev#93932:
Fixed void-safety issue introduced in rev#92560 where `l_rows' was potentially not set in `resize_column_to_width'. I've changed that by checking against the thing we want to use and verifying it is attached.

---

Revision 93930 - Directory Listing
Modified Wed Jan 8 13:37:01 2014 UTC (5 years, 11 months ago) by polikarn

Made MML a separate cluster in base-eve.

---

Revision 93929 - Directory Listing
Modified Wed Jan 8 13:12:05 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis:

- redesign of CFG rules and iteration
- Reaching Definitions analysis
- 'unneeded helper variable' rule

---

Revision 93914 - Directory Listing
Modified Tue Jan 7 16:52:46 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: improved analysis with cached results

---

Revision 93899 - Directory Listing
Modified Mon Jan 6 15:12:22 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: 'feature never called' fix

---

Revision 93898 - Directory Listing
Modified Mon Jan 6 14:50:00 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: better violation fixing

---

Revision 93897 - Directory Listing
Modified Mon Jan 6 13:10:42 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: Caching functionality (not in use though); bug fixes.

---

Revision 93896 - Directory Listing
Modified Sun Jan 5 22:19:12 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis:

- 'unneeded parentheses' rule
- command line bugfix
- testing

---

Revision 93895 - Directory Listing
Modified Sun Jan 5 17:15:03 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: command line

- argument for restoring default preferences

---

Revision 93894 - Directory Listing
Modified Sat Jan 4 16:38:46 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: bug fixes

---

Revision 93893 - Directory Listing
Modified Sat Jan 4 12:42:07 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: fixing violations using additional text formatter

---

Revision 93867 - Directory Listing
Modified Thu Jan 2 17:44:10 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis:

- rule violation fixes
  - GUI
  - example fix (unused argument)

---

Revision 93866 - Directory Listing
Modified Wed Jan 1 15:23:02 2014 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: (prototype) rule violation fixing

---

Revision 93857 - Directory Listing
Modified Tue Dec 31 16:21:31 2013 UTC (5 years, 11 months ago) by polikarn

Added observer with inheritance example. Changed handling of status creator. Verifying default_create.

---

Revision 93856 - Directory Listing
Modified Tue Dec 31 13:59:41 2013 UTC (5 years, 11 months ago) by polikarn

Adding special properties of subjects and observers to the user_inv frame axiom. Removed unused code.

---

Revision 93840 - Directory Listing
Modified Mon Dec 30 17:54:41 2013 UTC (5 years, 11 months ago) by polikarn

Added frame axiom for user_inv; translation of frozen classes; adapted SC examples to work with inheritance.

---

Revision 93833 - Directory Listing
Modified Sun Dec 29 22:29:08 2013 UTC (5 years, 11 months ago) by polikarn

Basic support for inheritance; static semantics for inv_without; some tests.

---

Revision 93825 - Directory Listing
Modified Fri Dec 27 07:35:02 2013 UTC (5 years, 11 months ago) by jasonw

<<Merged from trunk#93824.>>

---

Revision 93812 - Directory Listing
Modified Thu Dec 26 18:08:04 2013 UTC (5 years, 11 months ago) by polikarn

More general loop variants: multiple components, different types, checked by default, variant inference. Refactored loop processing into multiple subroutines.

---

Revision 93811 - Directory Listing
Modified Wed Dec 25 14:07:47 2013 UTC (5 years, 11 months ago) by polikarn

Additional admissibility checks A4 and A5 that allow relaxed checks when updating subjects or observers; added attachment axioms for built-in attributes.

---

Revision 93790 - Directory Listing
Modified Mon Dec 23 16:51:45 2013 UTC (5 years, 11 months ago) by polikarn

Added Eiffel equivalents for writable checks and in_domain; added line numbers to validity errors; bugfix: adding type when doing class check for an empty class.

---

Revision 93789 - Directory Listing
Modified Mon Dec 23 14:28:02 2013 UTC (5 years, 11 months ago) by polikarn

Refactoring: introduced expression comparison.

---

Revision 93788 - Directory Listing
Modified Mon Dec 23 14:12:40 2013 UTC (5 years, 11 months ago) by alexk

Refactored alias analyzer to be a root class for different classes of the analysis: relational and graph-based.
Factored out change analysis from alias analysis for better modularity and reusability.
Removed initial version of change analysis that is no longer used.

---

Revision 93787 - Directory Listing
Modified Mon Dec 23 14:07:24 2013 UTC (5 years, 11 months ago) by alexk

Added a feature to extend collection of nested context keepers with another one.

---

Revision 93786 - Directory Listing
Modified Mon Dec 23 13:51:03 2013 UTC (5 years, 11 months ago) by polikarn

Bugfix: when adding default clauses to the invariant, excluded clauses count. Added assignments to implicit ghost sets on call to Current.wrap.

---

Revision 93780 - Directory Listing
Modified Fri Dec 20 15:08:05 2013 UTC (5 years, 11 months ago) by jasonw

<<Merged from trunk#93779.>>

---

Revision 93775 - Directory Listing
Modified Thu Dec 19 19:52:44 2013 UTC (5 years, 11 months ago) by polikarn

Added modify clauses for loops.

---

Revision 93758 - Directory Listing
Modified Wed Dec 18 11:41:28 2013 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: cont. rule implementation

---

Revision 93757 - Directory Listing
Modified Wed Dec 18 08:27:25 2013 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: 'TODO' rule

---

Revision 93750 - Directory Listing
Modified Tue Dec 17 19:58:56 2013 UTC (5 years, 11 months ago) by polikarn

Generating type properties for set and sequence arguments.

---

Revision 93747 - Directory Listing
Modified Tue Dec 17 16:50:19 2013 UTC (5 years, 11 months ago) by polikarn

Bugfix: termination for argumentless routines. Added explicit non-termination.

---

Revision 93745 - Directory Listing
Modified Tue Dec 17 14:12:29 2013 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: 'deeply nested if' rule

---

Revision 93743 - Directory Listing
Modified Tue Dec 17 13:24:11 2013 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: 'count equals zero' rule

---

Revision 93738 - Directory Listing
Modified Mon Dec 16 16:46:59 2013 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: new rule

- from loop can be transformed into across loop

---

Revision 93737 - Directory Listing
Modified Mon Dec 16 15:15:42 2013 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: 'short circuit if' rule

---

Revision 93736 - Directory Listing
Modified Mon Dec 16 14:18:54 2013 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: 'avoid not-equal comparison in if-else' rule

---

Revision 93735 - Directory Listing
Modified Mon Dec 16 13:19:17 2013 UTC (5 years, 11 months ago) by julian

AutoProof: fixed typo.

---

Revision 93734 - Directory Listing
Modified Mon Dec 16 13:02:32 2013 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: 'empty effective routine' rule

---

Revision 93733 - Directory Listing
Modified Mon Dec 16 12:32:04 2013 UTC (5 years, 11 months ago) by polikarn

Changed handling of default initialization in creators: free preconditions instead of assignment; precondition is_open now cannot be disabled since there is no choice.

---

Revision 93732 - Directory Listing
Modified Mon Dec 16 12:07:49 2013 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: 'attribute to local' rule

---

Revision 93731 - Directory Listing
Modified Mon Dec 16 09:25:16 2013 UTC (5 years, 11 months ago) by polikarn

Bugfix in precondition predicate generation. Fixed tests.

---

Revision 93730 - Directory Listing
Modified Sun Dec 15 17:27:06 2013 UTC (5 years, 11 months ago) by polikarn

Added more features to sequences and sets and more termination tests.

---

Revision 93728 - Directory Listing
Modified Sun Dec 15 15:00:11 2013 UTC (5 years, 11 months ago) by polikarn

Arguments as default variants.

---

Revision 93727 - Directory Listing
Modified Sun Dec 15 14:28:29 2013 UTC (5 years, 11 months ago) by polikarn

Bugfix: using custom equality for termination checks.

---

Revision 93726 - Directory Listing
Modified Sun Dec 15 12:57:21 2013 UTC (5 years, 11 months ago) by polikarn

Checking preconditions of functionals.

---

Revision 93718 - Directory Listing
Modified Fri Dec 13 17:11:51 2013 UTC (5 years, 11 months ago) by julian

AutoProof: added partial invariant admissibility check.

---

Revision 93717 - Directory Listing
Modified Fri Dec 13 17:10:47 2013 UTC (5 years, 11 months ago) by polikarn

Checking that creators are only used for creation.

---

Revision 93716 - Directory Listing
Modified Fri Dec 13 16:55:19 2013 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: GUI: tooltip with general rule description.

---

Revision 93715 - Directory Listing
Modified Fri Dec 13 16:48:35 2013 UTC (5 years, 11 months ago) by polikarn

Allowing checks in functionals.

---

Revision 93714 - Directory Listing
Modified Fri Dec 13 16:46:20 2013 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: 'inspect instructions' rule

---

Revision 93713 - Directory Listing
Modified Fri Dec 13 16:24:13 2013 UTC (5 years, 11 months ago) by polikarn

Removed some unnecessary checks, added semantic warnings.

---

Revision 93712 - Directory Listing
Modified Fri Dec 13 16:13:09 2013 UTC (5 years, 11 months ago) by zurfluhs

Code Analysis: Rules

- simplifiable boolean
- self-comparison
- wrong loop iteration
- Control Flow Graph: refactoring

---

Revision 93708 - Directory Listing
Modified Fri Dec 13 09:18:59 2013 UTC (5 years, 11 months ago) by julian

AutoProof: added additional context information for a verification result.

---

Revision 93706 - Directory Listing
Modified Thu Dec 12 22:19:59 2013 UTC (5 years, 11 months ago) by polikarn

Refactoring of the feature translation process; functional features now have boogie procedures to perform checks (e.g. termination).

---

Revision 93705 - Directory Listing
Modified Thu Dec 12 16:10:24 2013 UTC (5 years, 11 months ago) by julian

AutoProof: Added skeleton for invariant admissibility check.

---

Revision 93704 - Directory Listing
Modified Thu Dec 12 15:02:44 2013 UTC (5 years, 11 months ago) by polikarn

Decreases checks (except functional features).

---

Revision 93694 - Directory Listing
Modified Wed Dec 11 15:38:10 2013 UTC (6 years ago) by julian

AutoProof: fixed type comparison.

---

Revision 93685 - Directory Listing
Modified Tue Dec 10 16:51:16 2013 UTC (6 years ago) by zurfluhs

Code Analysis: minor

---

Revision 93684 - Directory Listing
Modified Tue Dec 10 16:39:44 2013 UTC (6 years ago) by julian

AutoProof: added line number information to command line output.

---

Revision 93683 - Directory Listing
Modified Tue Dec 10 16:26:29 2013 UTC (6 years ago) by zurfluhs

Code Analysis: 'Missing is_equal redefinition' rule

---

Revision 93681 - Directory Listing
Modified Tue Dec 10 14:20:43 2013 UTC (6 years ago) by zurfluhs

Code Analysis: new rules

- very short identifier
- very long identifier

---

Revision 93679 - Directory Listing
Modified Tue Dec 10 09:02:04 2013 UTC (6 years ago) by polikarn

If-expression fix (duplicate of the fix in trunk).

---

Revision 93672 - Directory Listing
Modified Mon Dec 9 20:36:57 2013 UTC (6 years ago) by zurfluhs

Code Analysis: minor

---

Revision 93671 - Directory Listing
Modified Mon Dec 9 20:28:48 2013 UTC (6 years ago) by zurfluhs

Code Analysis: 'boolean comparison' rule

---

Revision 93670 - Directory Listing
Modified Mon Dec 9 19:42:02 2013 UTC (6 years ago) by zurfluhs

Code Analysis: 'boolean result' rule

---

Revision 93667 - Directory Listing
Modified Mon Dec 9 17:35:51 2013 UTC (6 years ago) by polikarn

Copied cleaned-up examples into the tests.

---

Revision 93665 - Directory Listing
Modified Mon Dec 9 16:43:50 2013 UTC (6 years ago) by polikarn

Added old function for old expressions in the body. Made the trigger of global more restrictive for performance purposes.

---

Revision 93664 - Directory Listing
Modified Mon Dec 9 16:08:07 2013 UTC (6 years ago) by julian

Removed eve proofs legacy code.

---

Revision 93663 - Directory Listing
Modified Mon Dec 9 15:19:36 2013 UTC (6 years ago) by zurfluhs

Code Analysis: 'feature not commented' rule

---

Revision 93662 - Directory Listing
Modified Mon Dec 9 14:12:17 2013 UTC (6 years ago) by zurfluhs

Code Analysis: 'feature section not commented' rule

---

Revision 93661 - Directory Listing
Modified Mon Dec 9 12:12:31 2013 UTC (6 years ago) by zurfluhs

Code Analysis: 'very big class' rule

---

Revision 93660 - Directory Listing
Modified Sat Dec 7 15:42:33 2013 UTC (6 years ago) by zurfluhs

Code Analysis: 'very big class' rule.

---

Revision 93659 - Directory Listing
Modified Sat Dec 7 15:07:49 2013 UTC (6 years ago) by zurfluhs

Code Analysis: 'routine too long' rule.

---

Revision 93643 - Directory Listing
Modified Fri Dec 6 17:18:30 2013 UTC (6 years ago) by polikarn

Adding subsumtion 0 to safety checks.

---

Revision 93641 - Directory Listing
Modified Fri Dec 6 16:32:17 2013 UTC (6 years ago) by polikarn

Relaxed preconditions for updating subjects and observers (needs new admissibility checks!). Removed the timeout.

---

Revision 93640 - Directory Listing
Modified Fri Dec 6 15:49:56 2013 UTC (6 years ago) by julian

AutoProof: finished refactoring of error display.

---

Revision 93639 - Directory Listing
Modified Fri Dec 6 12:19:52 2013 UTC (6 years ago) by julian

AutoProof: generate annotations for ownership calls.

---

Revision 93638 - Directory Listing
Modified Fri Dec 6 11:59:14 2013 UTC (6 years ago) by zurfluhs

Code Analysis: new rule & re-fixed false fix

---

Revision 93637 - Directory Listing
Modified Fri Dec 6 11:50:07 2013 UTC (6 years ago) by julian

AutoProof: added stop button.
AutoProof: improved error messages.

---

Revision 93635 - Directory Listing
Modified Fri Dec 6 07:00:12 2013 UTC (6 years ago) by jasonw

<<Merged from trunk#93634.>>

---

Revision 93633 - Directory Listing
Modified Fri Dec 6 01:24:52 2013 UTC (6 years ago) by julian

AutoProof: refactoring of error message display.

---

Revision 93627 - Directory Listing
Modified Thu Dec 5 16:42:21 2013 UTC (6 years ago) by julian

AutoProof: continued refactoring of output parser.

---

Revision 93626 - Directory Listing
Modified Thu Dec 5 11:38:31 2013 UTC (6 years ago) by zurfluhs

Code Analysis: fix

---

Revision 93625 - Directory Listing
Modified Thu Dec 5 09:53:20 2013 UTC (6 years ago) by zurfluhs

Code Analysis: 'variable not read' rule

---

Revision 93622 - Directory Listing
Modified Wed Dec 4 17:44:29 2013 UTC (6 years ago) by polikarn

Initialization for sequences + refactoring.

---

Revision 93620 - Directory Listing
Modified Wed Dec 4 17:18:30 2013 UTC (6 years ago) by julian

AutoProof: redirect Boogie output to file.

---

Revision 93619 - Directory Listing
Modified Wed Dec 4 14:20:22 2013 UTC (6 years ago) by zurfluhs

Code Analysis: fixes

---

Revision 93615 - Directory Listing
Modified Tue Dec 3 20:48:26 2013 UTC (6 years ago) by zurfluhs

Code Analysis: 'variable not read' rule

---

Revision 93609 - Directory Listing
Modified Tue Dec 3 17:31:51 2013 UTC (6 years ago) by zurfluhs

Code Analysis: fixes

- AST type recorder
- 'unused argument' rule

---

Revision 93608 - Directory Listing
Modified Tue Dec 3 16:15:29 2013 UTC (6 years ago) by zurfluhs

Code Analysis: CFG builder: fixes

---

Revision 93607 - Directory Listing
Modified Tue Dec 3 12:54:12 2013 UTC (6 years ago) by zurfluhs

Code Analysis: minor

---

Revision 93606 - Directory Listing
Modified Tue Dec 3 10:58:59 2013 UTC (6 years ago) by zurfluhs

Code Analysis:

- preferences: default values fix
- 'variable not read' rule: minor

---

Revision 93605 - Directory Listing
Modified Tue Dec 3 10:10:31 2013 UTC (6 years ago) by polikarn

Adding global heap property as a precondition for lemmas + refactoring.

---

Revision 93597 - Directory Listing
Modified Tue Dec 3 00:48:44 2013 UTC (6 years ago) by julian

AutoProof: special translation for lemma and functional

---

Revision 93595 - Directory Listing
Modified Mon Dec 2 19:22:22 2013 UTC (6 years ago) by polikarn

Generating attached/detachable axioms for set and sequence attributes.

---

Revision 93594 - Directory Listing
Modified Mon Dec 2 17:50:11 2013 UTC (6 years ago) by zurfluhs

Code Analysis:

- Control Flow Graph stuff updated
- 'Variable not read' rule updated

---

Revision 93593 - Directory Listing
Modified Mon Dec 2 16:49:23 2013 UTC (6 years ago) by julian

AutoProof: added base-eve precompile and eve start scripts.

---

Revision 93592 - Directory Listing
Modified Mon Dec 2 14:16:00 2013 UTC (6 years ago) by polikarn

Made if-expression semistrict.

---

Revision 93589 - Directory Listing
Modified Mon Dec 2 08:22:48 2013 UTC (6 years ago) by julian

AutoProof: fake implementation for model query.

---

Revision 93588 - Directory Listing
Modified Sun Dec 1 16:42:39 2013 UTC (6 years ago) by zurfluhs

Code Analysis: Control Flow Graphs (continued)

---

Revision 93587 - Directory Listing
Modified Sun Dec 1 15:18:38 2013 UTC (6 years ago) by polikarn

Bugfix: adding the class mentioned in an object test to the translation pool.

---

Revision 93583 - Directory Listing
Modified Fri Nov 29 18:50:14 2013 UTC (6 years ago) by polikarn

Sequence theory is now 1-based. Fixed unsoundness in loop writes. Optimized global invariant in the bg theory. OOM verifies.

---

Revision 93582 - Directory Listing
Modified Fri Nov 29 17:40:31 2013 UTC (6 years ago) by zurfluhs

Code Analysis: added (untested & unfinished) Control Flow Graph functionality

---

Revision 93581 - Directory Listing
Modified Fri Nov 29 16:58:23 2013 UTC (6 years ago) by julian

AutoProof: started refactoring of output parser.