@@ -587,6 +587,57 @@ private module CmdArguments {
587
587
* Synthesize literals from known constant strings.
588
588
*/
589
589
private module LiteralSynth {
590
+ pragma [ nomagic]
591
+ private predicate assignmentHasLocation (
592
+ Raw:: Scope scope , string name , File file , int startLine , int startColumn
593
+ ) {
594
+ Raw:: isAutomaticVariableAccess ( _, name ) and
595
+ exists ( Raw:: Ast n , Location loc |
596
+ scopeAssigns ( scope , name , n ) and
597
+ loc = n .getLocation ( ) and
598
+ file = loc .getFile ( ) and
599
+ startLine = loc .getStartLine ( ) and
600
+ startColumn = loc .getStartColumn ( )
601
+ )
602
+ }
603
+
604
+ pragma [ nomagic]
605
+ private predicate varAccessHasLocation (
606
+ Raw:: VarAccess va , File file , int startLine , int startColumn
607
+ ) {
608
+ exists ( Location loc |
609
+ loc = va .getLocation ( ) and
610
+ loc .getFile ( ) = file and
611
+ loc .getStartLine ( ) = startLine and
612
+ loc .getStartColumn ( ) = startColumn
613
+ )
614
+ }
615
+
616
+ /**
617
+ * Holds if `va` is an access to the automatic variable named `name`.
618
+ *
619
+ * Unlike `Raw::isAutomaticVariableAccess`, this predicate also checks for
620
+ * shadowing.
621
+ */
622
+ private predicate isAutomaticVariableAccess ( Raw:: VarAccess va , string name ) {
623
+ Raw:: isAutomaticVariableAccess ( va , name ) and
624
+ exists ( Raw:: Scope scope , File file , int startLine , int startColumn |
625
+ scope = Raw:: scopeOf ( va ) and
626
+ varAccessHasLocation ( va , file , startLine , startColumn )
627
+ |
628
+ // If it's a read then make sure there is no assignment precedeeding it
629
+ va .isReadAccess ( ) and
630
+ not exists ( int assignStartLine , int assignStartCoumn |
631
+ assignmentHasLocation ( scope , name , file , assignStartLine , assignStartCoumn )
632
+ |
633
+ assignStartLine < startLine
634
+ or
635
+ assignStartLine = startLine and
636
+ assignStartCoumn < startColumn
637
+ )
638
+ )
639
+ }
640
+
590
641
private class LiteralSynth extends Synthesis {
591
642
final override predicate isRelevant ( Raw:: Ast a ) {
592
643
exists ( Raw:: VarAccess va | a = va |
@@ -598,7 +649,7 @@ private module LiteralSynth {
598
649
or
599
650
Raw:: isEnvVariableAccess ( va , _)
600
651
or
601
- Raw :: isAutomaticVariableAccess ( va , _)
652
+ isAutomaticVariableAccess ( va , _)
602
653
)
603
654
}
604
655
@@ -628,7 +679,7 @@ private module LiteralSynth {
628
679
Raw:: isEnvVariableAccess ( va , s ) and
629
680
child = SynthChild ( EnvVariableKind ( s ) )
630
681
or
631
- Raw :: isAutomaticVariableAccess ( va , s ) and
682
+ isAutomaticVariableAccess ( va , s ) and
632
683
child = SynthChild ( AutomaticVariableKind ( s ) )
633
684
)
634
685
}
0 commit comments