From 4637db06583bc250b96e6145fc7bac9e16c730df Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 1 Aug 2017 11:10:01 +0200 Subject: Fixes is_accessed_by. CNE_01700 is not working. The BCE has been updated to include a group of items that should be tagged by the CNE_01700 rule. However, it's not happening. I don't see anything wrong with the way the CNE_01700 rule is written and a quick overview of the generated model would lead me to conclude that it indeed should tag something. Likely there are still issues with the way properties are turned into Kodkod formulas. --- ast-to-instr/src/VHDLNode.java | 14 + ast-to-instr/src/VHDLProcess.java | 56 - ast-to-instr/src/VHDLSSASNode.java | 23 +- data/ast/best_chronometer_ever.xml | 22389 ++++++++++++++----------------- data/level/structural_level.lvl | 3 + data/property/cnes/CNE_01700.pro | 76 +- instr-to-kodkod/src/StringManager.java | 9 + 7 files changed, 10029 insertions(+), 12541 deletions(-) diff --git a/ast-to-instr/src/VHDLNode.java b/ast-to-instr/src/VHDLNode.java index b05f08c..36ba028 100644 --- a/ast-to-instr/src/VHDLNode.java +++ b/ast-to-instr/src/VHDLNode.java @@ -69,6 +69,13 @@ public abstract class VHDLNode extends ParsableXML Strings.get_id_from_string(Integer.toString(i)), elements.get(i) ); + + Predicates.add_entry + ( + "is_accessed_by", + elements.get(i), + parent_id + ); } } @@ -111,6 +118,13 @@ public abstract class VHDLNode extends ParsableXML Strings.get_id_from_string(Integer.toString(i)), elements.get(i) ); + + Predicates.add_entry + ( + "is_accessed_by", + elements.get(i), + parent_id + ); } } } diff --git a/ast-to-instr/src/VHDLProcess.java b/ast-to-instr/src/VHDLProcess.java index 1146f3f..2eae165 100644 --- a/ast-to-instr/src/VHDLProcess.java +++ b/ast-to-instr/src/VHDLProcess.java @@ -10,7 +10,6 @@ import java.util.Stack; public class VHDLProcess extends ParsableXML { private static final XPathExpression XPE_FIND_SL_ELEMENTS; - private static final XPathExpression XPE_FIND_NE_IN_PROCESS; private static final XPathExpression XPE_FIND_START_NODE; static @@ -21,12 +20,6 @@ public class VHDLProcess extends ParsableXML "(./sensitivity_list/el/named_entity | ./sensitivity_list/el[@ref])" ); - XPE_FIND_NE_IN_PROCESS = - XMLManager.compile_or_die - ( - ".//*[@kind=\"simple_name\"]/named_entity" - ); - XPE_FIND_START_NODE = XMLManager.compile_or_die ( @@ -80,7 +73,6 @@ public class VHDLProcess extends ParsableXML handle_predicate_is_explicit_process(local_id); handle_predicate_is_in_sensitivity_list(local_id); - handle_predicate_is_accessed_by(local_id); /** Children ************************************************************/ handle_child_node(local_id, waiting_list); @@ -407,54 +399,6 @@ public class VHDLProcess extends ParsableXML } } - private void handle_predicate_is_accessed_by - ( - final IDs local_id - ) - throws XPathExpressionException - { - final NodeList items; - final int items_count; - - items = - (NodeList) XPE_FIND_SL_ELEMENTS.evaluate - ( - xml_node, - XPathConstants.NODESET - ); - - items_count = items.getLength(); - - for (int i = 0; i < items_count; ++i) - { - final String xml_id; - - xml_id = - XMLManager.get_attribute - ( - items.item(i), - "ref" - ); - - if (!Main.node_is_function_or_literal(xml_id)) - { - Predicates.add_entry - ( - "is_accessed_by", - Waveforms.get_associated_waveform_id - ( - IDs.get_id_from_xml_id - ( - xml_id, - null - ) - ), - local_id - ); - } - } - } - /***************************************************************************/ /** Children ***************************************************************/ /***************************************************************************/ diff --git a/ast-to-instr/src/VHDLSSASNode.java b/ast-to-instr/src/VHDLSSASNode.java index 944ad18..fd43f28 100644 --- a/ast-to-instr/src/VHDLSSASNode.java +++ b/ast-to-instr/src/VHDLSSASNode.java @@ -170,6 +170,7 @@ public class VHDLSSASNode extends VHDLNode ) throws XPathExpressionException { + final IDs target_id; Node target; target = @@ -221,11 +222,7 @@ public class VHDLSSASNode extends VHDLNode ); } - Predicates.add_entry - ( - output, - "expr_writes", - local_id, + target_id = Waveforms.get_associated_waveform_id ( IDs.get_id_from_xml_id @@ -233,7 +230,21 @@ public class VHDLSSASNode extends VHDLNode XMLManager.get_attribute(target, "id"), (String) null ) - ) + ); + + Predicates.add_entry + ( + output, + "expr_writes", + local_id, + target_id + ); + + Predicates.add_entry + ( + "is_accessed_by", + target_id, + parent_id ); } diff --git a/data/ast/best_chronometer_ever.xml b/data/ast/best_chronometer_ever.xml index 4b597a8..89491ae 100644 --- a/data/ast/best_chronometer_ever.xml +++ b/data/ast/best_chronometer_ever.xml @@ -6124,7 +6124,7 @@ seen_flag="false" has_parameter="false" hide_implicit_flag="false" pure_flag="false" foreign_flag="false" visible_flag="true" - is_within_flag="false" use_flag="true" + is_within_flag="false" use_flag="false" resolution_function_flag="false" has_pure="false" has_body="false" wait_state="unknown" all_sensitized_state="???"> @@ -8176,58 +8176,58 @@ identifier="work" date="10" library_directory="" elab_flag="false" visible_flag="true"> - - - + - - - + + - - - + - - - + - + - - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - + - + - - - + - - + - + - - - + - - - + + + - + - - - + + + + + + + + + + + + + + + + + + + - - - + + + - + - - + - - - + - - - - + + + - - + - - - + + + - - - + - - - + + + - - + - - - + + + - - - - + - - - + + - - - - - + + + - - + + - - - + + - - - - - + + + - - + - - - + + + - - - - - + + + - - + - - - + + + - - - + - - - + + + - - - - + + - - - + + + - + @@ -8656,164 +8693,164 @@ - - + - - - + + + - - - - + + + - - + - - - + - - - - + + + - - + - - - + + + - - - + - - - + + + - - + - - - + + + - - - - + - - - + + - - - - - + + + - - + + - - - + - - - + + + - - - - - + + + @@ -8824,201 +8861,369 @@ - - + - - - + + + - - - - + + + - - + - - - + - - - + + + - - + - - + - - - + + + - - + - - - + + + - - - + + + - - + - - + - - - + - - - + + + - - + - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + - - + - - + + - + - + - - - + - - - + + - - - + - - - + - + - - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + - + - + - - + + - @@ -9159,10 +9364,10 @@ - + - - - - + + - + - + - - + + - @@ -9203,10 +9408,10 @@ - + - - - - + + - + - + - - + + - @@ -9247,10 +9452,10 @@ - + - - - - + + - + - + - - + + - @@ -9291,86 +9496,86 @@ - + - + - + - - - + - - + - + - - - + - - - + + + - + - - - - + + - + - + - - + + - @@ -9379,40 +9584,40 @@ - + - - - - + + - + - + - - + + - @@ -9421,40 +9626,40 @@ - + - - - - + + - + - + - - + + - @@ -9463,40 +9668,40 @@ - + - - - - + + - + - + - - + + - @@ -9505,66 +9710,66 @@ - + - - + - - - + - - - - + + + - - + - - - + + + - - - + + - - - + + + - - + @@ -9572,167 +9777,167 @@ - - - - + - - - + + - - - - - + + + - - + + - - - + + - - - - - + + + - - + - - - + + + - - - - - + + + - - + - - - + + + - - - + - - - - + + + - - - - + - - - + + + - - + @@ -9741,55 +9946,54 @@ - - - - + - - - + + + - - - - - - + + + - @@ -9809,81 +10013,81 @@ - - - - - + + + + + - - - - + + + + - - + - - - + - - - - + + + - - + - - - + + + - - - + + - - - + + + - - + @@ -9891,135 +10095,135 @@ - - - - + - - - + + - - - - - + + + - - + + - - - + + - - - - - - + + + - - + - - - + + + - - - - - + + + - - + - - - + + + - - - - - + + + - @@ -10027,60 +10231,60 @@ - - - + - - - - + + + - - - - + - - - + + + - - + @@ -10089,55 +10293,54 @@ - - - - + - - - + + + - - - - - - + + + - @@ -10157,81 +10360,81 @@ - - - - - + + + + + - - - - + + + + - - + - - - + - - - - + + + - - + - - - + + + - - - + + - - - + + + - - + @@ -10239,142 +10442,142 @@ - - - - + - - - + + - - - - - + + + - - + + - - - + + - - - - - - - + + + - - + - - - + + + - - - - - + + + - - + - - - + + + - - - - - + + + - @@ -10382,24 +10585,24 @@ - - - - - + + + - @@ -10407,60 +10610,60 @@ - - - + - - - - + + + - - - - + - - - + + + - - + @@ -10469,55 +10672,54 @@ - - - - + - - - + + + - - - - - - + + + - @@ -10537,81 +10739,81 @@ - - - - - + + + + + - - - - + + + + - - + - - - + - - - - + + + - - + - - - + + + - - - + - - - + + + - - + @@ -10619,176 +10821,174 @@ - - - - + - - - + + - - - - - + + + - - + + - - - + + - - - - + file="src/time_wizard.vhd" line="109" + col="35" expr_staticness="none"> - - - - + + + - - + - - - + + + - + file="src/time_wizard.vhd" line="110" + col="35" expr_staticness="none"> - - - - + + + - - + - - - + + + - - - - - + + + - - - - - - + + + - @@ -10796,24 +10996,24 @@ - - - - - + + + - @@ -10821,48 +11021,47 @@ - - - + - - - + + + - - + file="src/time_wizard.vhd" line="116" + col="32" expr_staticness="none"> - - - - + + + - @@ -10879,191 +11078,191 @@ - - - - - + + + + + - - - - + + + + - - + - - - + - - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - + + - - - + + + - - + - - - + + + - - - - + - + - - + - - - + + + @@ -11072,1041 +11271,1037 @@ - - - - - + + + + + - - + - + - + - - + - - - + - - - + + + - - + - - - + + + - - + + - - + - - + - - - + - - - + + + - - + - - - + + + - - + + - - + - - + - - - + - - - + + + - - + - - - + + + - - + + - - + - - + - - - + - - - + + + - - + - - - + + + - - + + - - + - - + - - - + - - - + + + - - + - - - + + + - - + + - - + - - + + - + - + - - - + - - - + + - - - + - - - + - + - - + + - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - + + + - - - + + + - + + + + + + + + + + + + + + + + + + + - + + + + + - - - - - - - - - - - - - - - + + + - - - + + + - + + + + + + + + + + + + + + + + + + + - + + + + + - - - + + - - - - + + + - - + - - + - - - + + - - - + + + - + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + - - - - - - + expr_staticness="global" name_staticness="local"> + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + - - - - - - + expr_staticness="global" name_staticness="local"> + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + has_signal_flag="true" type_staticness="local"> + + - - - - + + - - + + - @@ -12115,542 +12310,559 @@ - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - - - - - - - - - - - - - - - - - - + - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - - + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - - - - + + - - + - - - - - - - - - - - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - - - - + + - - + - - - - - - - - - - - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - - - - + + - - + + - - - - - - - - - - - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + @@ -12658,593 +12870,116 @@ - - - - + + + - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - + - - - + + + - + - - - + - - - + + + - + - - - - - - + + + + + + + + + + + + + + + + + + + - + - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - - - - + + + + + + + + + + + + + - - - + + + - - - - - - - - - - - - - - - - - - - + - + - - - + - - - - + + + - - + - - + + - + - - + + - - - + + + - + - + + - + - - - + + - - + - + - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - + + + + + + + + + + + - - - - - - - - + + + + + + + + + + + - - - - - - - - + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + - - - + + + - + - - - + - - - + + + - + - - - + - - + has_signal_flag="true" type_staticness="global"> + + - - + + + + - - + + - @@ -13614,3105 +13673,1129 @@ - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + - + + + + + + - + + + + - + + + + - - - - - - - - - - - - - + + + + - - - - - - - - - - - + + + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - + + + + + + - - - - - - - - - - - + + + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - + + + + + + - + + + + + + - - + + - + - + - - - + - - - + + - - - + - - - + - + - - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - + - + - - - + - - + - + - - - + - - - + + + - + - - - + - - - + + + - + - - + - - - + - - - - + + + - - + - - - + + + - - - + - - - + + + - - + - - - + + + - - - - - + + - - + + - - - - - + + + - - + + - - - + - - - + + + - - - - - + + + @@ -17009,166 +15090,164 @@ - - + - - - + + + - - - - + + + - - + - - - + - - - - + + + - - + - - - + + + - - - + - - - + + + - - + - - - + + + - - - - - + + - - + + - - - - - + + + - - + + - - - + - - - + + + - - - - - + + + @@ -17179,1531 +15258,925 @@ - - + - - - + + + - - - - + + + - - + - - - + - - - + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + - - - - + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + - - - + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + - + - + - + - - - + - - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - + - - - - - - - - - - - + + + + + + + + + + + + + + - - - - + + + + - - - - - - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - + + + + + - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - - - - - - + + + + + + + + + + + + + + + + + + + + - - + + + - - + + + + + + + - - + + - + - + - - - + + - - - + + - - - + + - - - + - + - - - - - - - - - - - - - - - - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - + + + - + - - - + + - - - + + + - + - - - - - - - - - - - - - - - - - - + - - + has_signal_flag="true" type_staticness="local"> + + - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - @@ -18873,1579 +16717,1735 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + - - - + + - - - + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - + + - + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - + + + - - - - - - - - - - - - - - - - - - - - - - + + + + + - - + + - + - - + + + + + + + - - - - - - - - - - - - - - - - - - - - - - + + + + + - - + + - + - - + + + + + + + - - - - - - - - - - - - - - - - - - - - - - + + + + + - - + + - + - - + + + + + + + - - - - - - - - - - - - - - - - - - - - - - + + + + + - - + + - + - - + + + + + + + - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - + + + - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - + + + - - - - - - - - - - - - - - - - - - - - - - + + + + + - - + + - + - - + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + - - + + - + - - + + + + + + + - - - - - - - - - - - - - - - - - - + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + - - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + - - + + + + + + + + + + - - - + + - - + + - - - - - + + + - - - - + + + - - - - - + + + - - - - + + + - - + + + + + - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - + + + - - - - - + + + - - - - + + + - - - - - + + + - - - - + + + - - - - - + + + - - - - + + + - - - - - - + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - - - - + + + + + + + + + + + - + - - - - - - + + + + + + + + + + + + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - + - - - - - - - - - - - - - - - - + - - - + + + + + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + + + + + + + + + + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + - + - + - + - - - + - - - + - + - + - + - - + - - - + - + - + - + - - + - - - + - + - + - + - - + - - - + - + - + - + - - + - - - + - + - + - + - - + - - - + - + - + - + - - + - - - + - + - + - + - - + - - - + - + - - - + - - + - - + + - - - + + - - - + + - - - + + - - - + + - - - + + - - - + + - - - + + - - - + + - - - - + + + - - + + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - - + - - + @@ -22580,24 +20089,24 @@ - - - - + + + - - - - + + + + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - - + + - - + - - + - - - + + - - + - - + - - - + + - - + - - + - - - + + - - + - - + - - - + + - - - + - - - + + + - + - - - - + + + - - - + - - + - - - + + + - - - + + - - - + + + - + - - - + - - + @@ -23038,24 +20547,24 @@ - - - - + + + - - - - + + + + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - - + + - - + - - + - - - + + - - + - - + - - - + + - - + - - + - - - + + - - + - - + - - - + - - - - - + + + - - - - + + + - - - + + + - - - - + + + - - - + + - - - + + + - + - - - + - - - - - + + + - - - - + + + - - - + + + - - - - + + + - - - + + - - - + + + - + - - - + - - - - - + + + - - - - + + + - - - + + + - - - - + + + - - - + + - - - + + + - + - - - + - - - - - + + + - - - - + + + - - - + + + - - - - + + + - - - + + - - - + + + - + - - - + + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - + - - - + - - - + + + - + - - - + @@ -24807,7 +22316,7 @@ - @@ -24818,7 +22327,7 @@ - @@ -24827,10 +22336,10 @@ - - + - - - + - - - + + + - + - - - + @@ -24876,7 +22385,7 @@ - @@ -24887,7 +22396,7 @@ - @@ -24896,10 +22405,10 @@ - - + - - - + - - - + + + - + - - - + @@ -24945,7 +22454,7 @@ - @@ -24956,7 +22465,7 @@ - @@ -24965,10 +22474,10 @@ - - - + + - - - + @@ -24998,19 +22507,19 @@ - - - - + + + - - - + + - - - + @@ -25040,19 +22549,19 @@ - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + @@ -25125,19 +22634,19 @@ - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + @@ -25338,19 +22847,19 @@ - - - - + + + - - - + + - - - + @@ -25380,19 +22889,19 @@ - - - - + + + - - - + + - - - + @@ -25422,19 +22931,19 @@ - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + @@ -25592,19 +23101,19 @@ - - - - + + + - - - + + - - - + @@ -25634,19 +23143,19 @@ - - - - + + + - - - + + - - - + @@ -25676,19 +23185,19 @@ - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + @@ -25846,19 +23355,19 @@ - - - - + + + - - - + + - - - + @@ -25888,19 +23397,19 @@ - - - - + + + - - - + + - - - + @@ -25930,19 +23439,19 @@ - - - - + + + - - + - - - + - - - + + + - + - @@ -25983,10 +23492,10 @@ - - + - - - + - - - + + + - + - @@ -26027,10 +23536,10 @@ - - + - - - + - - - + + + - + - @@ -26070,10 +23579,10 @@ - - + - - - + - - - + + + - + - @@ -26113,10 +23622,10 @@ - - + - - - + - - - + + + - + - @@ -26157,190 +23666,188 @@ - - + + - + - - + - - - + - + - + - - + - - - + - + - + - - + - - - + - + - - + - - + - - - + - + - + - - + - - - + - + - + - - + - - - + - + - + - - + - - - + - + - + - - + - - - + - + - - + diff --git a/data/level/structural_level.lvl b/data/level/structural_level.lvl index 40aa455..dab377b 100644 --- a/data/level/structural_level.lvl +++ b/data/level/structural_level.lvl @@ -131,6 +131,9 @@ ;;;; String ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (add_predicate string_matches string string) +;; is_accessed_by's signature must match is_read_element and +;; is_written_element's +(add_predicate is_accessed_by string process) ;;;; Type ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (add_predicate is_approved_type type) diff --git a/data/property/cnes/CNE_01700.pro b/data/property/cnes/CNE_01700.pro index a0cb792..d254ad1 100644 --- a/data/property/cnes/CNE_01700.pro +++ b/data/property/cnes/CNE_01700.pro @@ -3,10 +3,46 @@ (x_re waveform CNE_01700_HAS_BAD_NAME) ) (and - (not (string_matches [identifier x_re] ".*_re")) + (not (string_matches [identifier [is_waveform_of x_re]] ".*_re")) (exists x waveform (exists x_r1 waveform (and + (exists ps2 process + (and + (is_in_sensitivity_list x_r1 ps2) + (is_in_sensitivity_list x ps2) + (is_accessed_by x_re ps2) + (CTL_verifies ps2 + (AF + (and + (expr_writes x_re) + (is_read_element "0" "and") + (or + (and + (is_read_structure "(?(??)?)") + (is_read_element "1" "not") + (is_read_element "2" x_r1) + (is_read_element "3" x) + ) + (and + (is_read_structure "(??(??))") + (is_read_element "1" x) + (is_read_element "2" "not") + (is_read_element "3" x_r1) + ) + ) + (AX + (not + (EF + (expr_writes x_r1) + ) + ) + ) + ) + ) + ) + ) + ) (exists ps1 process (and (is_accessed_by x_r1 ps1) @@ -28,7 +64,7 @@ (is_read_element "1" clk1) (EX (and - (has_option "COND_WAS_TRUE") + (has_option "cond_was_true") (does_not_reach_parent_before (and (expr_writes x_r1) @@ -99,42 +135,6 @@ ) ) ) - (exists ps2 process - (and - (is_in_sensitivity_list x_r1 ps2) - (is_in_sensitivity_list x ps2) - (is_accessed_by x_re ps2) - (CTL_verifies ps2 - (AF - (and - (expr_writes x_re) - (is_read_element "0" "and") - (or - (and - (is_read_structure "(?(??)?)") - (is_read_element "1" "not") - (is_read_element "2" x_r1) - (is_read_element "3" x) - ) - (and - (is_read_structure "(??(??))") - (is_read_element "1" x) - (is_read_element "2" "not") - (is_read_element "3" x_r1) - ) - ) - (AX - (not - (EF - (expr_writes x_r1) - ) - ) - ) - ) - ) - ) - ) - ) ) ) ) diff --git a/instr-to-kodkod/src/StringManager.java b/instr-to-kodkod/src/StringManager.java index 9d73dd6..e94a7af 100644 --- a/instr-to-kodkod/src/StringManager.java +++ b/instr-to-kodkod/src/StringManager.java @@ -75,6 +75,15 @@ public class StringManager { if (p.matcher(c.getKey()).matches()) { + System.out.println + ( + "[D] \"" + + c.getValue() + + "\" matches pattern \"" + + p.pattern() + + "\"." + ); + rp.add_member ( new String[] -- cgit v1.2.3-70-g09d2